Lebesgue measure on ℂⁿ as the Haar measure of its standard real basis

Category: 1-Mathlib (CSD-free; upstream targets Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean and Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean).

Fin n → ℂ carries the product Lebesgue measure volume, and EuclideanSpace ℂ (Fin n) the volume of its real inner-product structure. Both are the Haar measure of the standard real basis (e_j, i·e_j)_j, and the identification ofLp between the two spaces is volume preserving.

• parallelepiped_pi_basis — a product basis has the product parallelepiped;
• Complex.volume_parallelepiped_basisOneI — Lebesgue measure on ℂ gives the unit square of basisOneI mass 1 (basisOneI is the orthonormal basis orthonormalBasisOneI);
• ★ Complex.addHaar_pi_basisOneI_reindex — the Haar measure of the standard real basis of Fin n → ℂ (any reindexing of Pi.basis fun _ => basisOneI) is Lebesgue measure;
• Complex.euclideanBasis n, Complex.euclideanOrthonormalBasis n — the same family in EuclideanSpace ℂ (Fin n), indexed by Fin (2 * n), as a basis and as Mathlib's product orthonormal basis Pi.orthonormalBasis of orthonormalBasisOneI;
• ★ Complex.measurePreserving_ofLp — ofLp : EuclideanSpace ℂ (Fin n) → (Fin n → ℂ) is volume preserving, the inner-product volume on the left and the product Lebesgue measure on the right.

theorem parallelepiped_pi_basis {ι : Type u_1} [Fintype ι] [DecidableEq ι] {η : ι → Type u_2} [(i : ι) → Fintype (η i)] {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module ℝ (M i)] (b : (i : ι) → Module.Basis (η i) ℝ (M i)) : parallelepiped ⇑(Pi.basis b) = Set.univ.pi fun (i : ι) => parallelepiped ⇑(b i)

The parallelepiped of a product basis is the product of the parallelepipeds.

theorem Complex.volume_parallelepiped_basisOneI : MeasureTheory.volume (parallelepiped ⇑basisOneI) = 1

Lebesgue measure on ℂ gives the unit square parallelepiped basisOneI mass 1: basisOneI is the orthonormal basis orthonormalBasisOneI.

theorem Complex.addHaar_pi_basisOneI_reindex {n : ℕ} {ι : Type u_1} [Fintype ι] (e : (_ : Fin n) × Fin 2 ≃ ι) : ((Pi.basis fun (x : Fin n) => basisOneI).reindex e).addHaar = MeasureTheory.volume

★ The Haar measure of the standard real basis of Fin n → ℂ is Lebesgue measure, for any indexing of the family (e_j, i·e_j)_j: the reindexing does not change the Haar measure, the product basis has the product unit cube, and each factor's unit square has Lebesgue mass 1.

def Complex.sigmaFinTwoEquiv (n : ℕ) : (_ : Fin n) × Fin 2 ≃ Fin (2 * n)

The index equivalence (Σ _ : Fin n, Fin 2) ≃ Fin (2 * n) behind the standard real basis.

Equations

• Complex.sigmaFinTwoEquiv n = (Equiv.sigmaEquivProd (Fin n) (Fin 2)).trans (finProdFinEquiv.trans (finCongr ⋯))

noncomputable def Complex.euclideanBasis (n : ℕ) : Module.Basis (Fin (2 * n)) ℝ (EuclideanSpace ℂ (Fin n))

The standard real basis (e_j, i·e_j)_j of EuclideanSpace ℂ (Fin n), indexed by Fin (2 * n).

Equations

• Complex.euclideanBasis n = ((Pi.basis fun (x : Fin n) => Complex.basisOneI).reindex (Complex.sigmaFinTwoEquiv n)).map (↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin n) => ℂ)).symm

theorem Complex.euclideanBasis_map_ofLp (n : ℕ) : (euclideanBasis n).map ↑(PiLp.continuousLinearEquiv 2 ℝ fun (x : Fin n) => ℂ) = (Pi.basis fun (x : Fin n) => basisOneI).reindex (sigmaFinTwoEquiv n)

theorem Complex.euclideanBasis_apply (n : ℕ) (c : Fin (2 * n)) : (euclideanBasis n) c = WithLp.toLp 2 (Pi.single ((sigmaFinTwoEquiv n).symm c).fst (basisOneI ((sigmaFinTwoEquiv n).symm c).snd))

noncomputable def Complex.euclideanOrthonormalBasis (n : ℕ) : OrthonormalBasis (Fin (2 * n)) ℝ (EuclideanSpace ℂ (Fin n))

The standard real basis of EuclideanSpace ℂ (Fin n) as an orthonormal basis: Mathlib's product Pi.orthonormalBasis of orthonormalBasisOneI, reindexed by Fin (2 * n).

Equations

• Complex.euclideanOrthonormalBasis n = (Pi.orthonormalBasis fun (x : Fin n) => Complex.orthonormalBasisOneI).reindex (Complex.sigmaFinTwoEquiv n)

theorem Complex.euclideanOrthonormalBasis_toBasis (n : ℕ) : (euclideanOrthonormalBasis n).toBasis = euclideanBasis n

Its underlying basis is euclideanBasis n.

theorem Complex.orthonormal_euclideanBasis (n : ℕ) : Orthonormal ℝ ⇑(euclideanBasis n)

The standard real basis of EuclideanSpace ℂ (Fin n) is orthonormal.

theorem Complex.measurePreserving_ofLp (n : ℕ) : MeasureTheory.MeasurePreserving WithLp.ofLp MeasureTheory.volume MeasureTheory.volume

★ ofLp : EuclideanSpace ℂ (Fin n) → (Fin n → ℂ) is volume preserving: the volume of the real inner-product structure on the left is the Haar measure of the orthonormal basis euclideanOrthonormalBasis n (OrthonormalBasis.addHaar_eq_volume), whose image is the standard real basis of Fin n → ℂ, whose Haar measure is Lebesgue measure.