Lebesgue measure on ℂ

In this file, we consider the Lebesgue measure on ℂ defined as the push-forward of the volume on ℝ² under the natural isomorphism and prove that it is equal to the measure volume of ℂ coming from its InnerProductSpace structure over ℝ. For that, we consider the two frequently used ways to represent ℝ² in mathlib: ℝ × ℝ and Fin 2 → ℝ, define measurable equivalences (MeasurableEquiv) to both types and prove that both of them are volume preserving (in the sense of MeasureTheory.measurePreserving).

def Complex.measurableEquivPi : ℂ ≃ᵐ (Fin 2 → ℝ)

Measurable equivalence between ℂ and ℝ² = Fin 2 → ℝ.

Equations

• Complex.measurableEquivPi = Homeomorph.toMeasurableEquiv (ContinuousLinearEquiv.toHomeomorph (LinearEquiv.toContinuousLinearEquiv (Basis.equivFun Complex.basisOneI)))

@[simp]

theorem Complex.measurableEquivPi_apply (a : ℂ) : Complex.measurableEquivPi a = ![a.re, a.im]

@[simp]

theorem Complex.measurableEquivPi_symm_apply (p : Fin 2 → ℝ) : Complex.measurableEquivPi.symm p = ↑(p 0) + ↑(p 1) * Complex.I

def Complex.measurableEquivRealProd : ℂ ≃ᵐ ℝ × ℝ

Measurable equivalence between ℂ and ℝ × ℝ.

Equations

• Complex.measurableEquivRealProd = Homeomorph.toMeasurableEquiv (ContinuousLinearEquiv.toHomeomorph Complex.equivRealProdCLM)

@[simp]

theorem Complex.measurableEquivRealProd_apply (a : ℂ) : Complex.measurableEquivRealProd a = (a.re, a.im)

@[simp]

theorem Complex.measurableEquivRealProd_symm_apply (p : ℝ × ℝ) : Complex.measurableEquivRealProd.symm p = { re := p.1, im := p.2 }

theorem Complex.volume_preserving_equiv_pi : MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivPi) MeasureTheory.volume MeasureTheory.volume

theorem Complex.volume_preserving_equiv_real_prod : MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivRealProd) MeasureTheory.volume MeasureTheory.volume