mathlib3 documentation

measure_theory.measure.lebesgue.complex

Lebesgue measure on ℂ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

Lebesgue measure on ℂ.

Equations
source
noncomputable def complex.measurable_equiv_pi  :
ℂ ≃ᵐ (fin 2 → ℝ)

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

Equations
source
noncomputable def complex.measurable_equiv_real_prod  :
ℂ ≃ᵐ ℝ × ℝ

Measurable equivalence between ℂ and ℝ × ℝ.

Equations
source
theorem complex.volume_preserving_equiv_pi  :
measure_theory.measure_preserving ⇑complex.measurable_equiv_pi measure_theory.measure_space.volume measure_theory.measure_space.volume
source
theorem complex.volume_preserving_equiv_real_prod  :
measure_theory.measure_preserving ⇑complex.measurable_equiv_real_prod measure_theory.measure_space.volume measure_theory.measure_space.volume