# 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

- Complex.measurableEquivPi = Complex.basisOneI.equivFun.toContinuousLinearEquiv.toHomeomorph.toMeasurableEquiv

## Instances For

@[simp]

@[simp]

theorem
Complex.measurableEquivPi_symm_apply
(p : Fin 2 → ℝ)
:

Complex.measurableEquivPi.symm p = ↑(p 0) + ↑(p 1) * Complex.I

Measurable equivalence between `ℂ`

and `ℝ × ℝ`

.

## Equations

- Complex.measurableEquivRealProd = Complex.equivRealProdCLM.toHomeomorph.toMeasurableEquiv

## Instances For

@[simp]

theorem
Complex.measurableEquivRealProd_apply
(a : ℂ)
:

Complex.measurableEquivRealProd a = (a.re, a.im)

@[simp]

theorem
Complex.measurableEquivRealProd_symm_apply
(p : ℝ × ℝ)
:

Complex.measurableEquivRealProd.symm p = { re := p.1, im := p.2 }

theorem
Complex.volume_preserving_equiv_pi :

MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivPi) MeasureTheory.volume MeasureTheory.volume

theorem
Complex.volume_preserving_equiv_real_prod :

MeasureTheory.MeasurePreserving (⇑Complex.measurableEquivRealProd) MeasureTheory.volume MeasureTheory.volume