mathlibdocumentation

measure_theory.measure.complex_lebesgue

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

@[protected, instance]
noncomputable def complex.measure_space  :

Lebesgue measure on ℂ.

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

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

Equations

Measurable equivalence between ℂ and ℝ × ℝ.

Equations