mathlib documentation


Lebesgue measure on #

In this file we define Lebesgue measure on . Since is defined as a structure as the push-forward of the volume on ℝ² under the natural isomorphism. There are (at least) two frequently used ways to represent ℝ² in mathlib: ℝ × ℝ and fin 2 → ℝ. We define measurable equivalences (measurable_equiv) to both types and prove that both of them are volume preserving (in the sense of measure_theory.measure_preserving).

noncomputable def complex.measurable_equiv_pi  :
≃ᵐ (fin 2)

Measurable equivalence between and ℝ² = fin 2 → ℝ.