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).

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

Equations
Instances For
@[simp]
theorem Complex.measurableEquivPi_apply (a : ) :
= ![a.re, a.im]
@[simp]
theorem Complex.measurableEquivPi_symm_apply (p : Fin 2) :
= (p 0) + (p 1) * Complex.I

Measurable equivalence between ℂ and ℝ × ℝ.

Equations
Instances For
@[simp]
theorem Complex.measurableEquivRealProd_apply (a : ) :
= (a.re, a.im)
@[simp]
theorem Complex.measurableEquivRealProd_symm_apply (p : ) :
= { re := p.1, im := p.2 }