Documentation

Mathlib.MeasureTheory.Measure.Lebesgue.Complex

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