Documentation

Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Invariant measure on the upper half-plane #

We equip the upper half-plane with a measure, defined as the restriction of the usual measure on ℂ weighted by the function 1 / (im z) ^ 2. We show that this measure is invariant under the action of GL(2, ℝ).

source
@[implicit_reducible]
noncomputable instance instMeasureSpaceComplex :
MeasureTheory.MeasureSpace ℂ
Equations
source
instance instFiniteDimensionalRealComplex :
FiniteDimensional ℝ ℂ
source
@[implicit_reducible]
noncomputable instance UpperHalfPlane.instMeasurableSpace :
MeasurableSpace UpperHalfPlane
Equations
source
instance UpperHalfPlane.instBorelSpace :
BorelSpace UpperHalfPlane
source
theorem UpperHalfPlane.measurableEmbedding_coe :
MeasurableEmbedding UpperHalfPlane.coe
source
theorem UpperHalfPlane.measurable_coe :
Measurable UpperHalfPlane.coe
source
@[implicit_reducible]
noncomputable instance UpperHalfPlane.instMeasureSpace :
MeasureTheory.MeasureSpace UpperHalfPlane

The invariant measure on the upper half-plane, defined by dx dy / y ^ 2.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem UpperHalfPlane.volume_def :
MeasureTheory.volume = (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume).withDensity fun (z : UpperHalfPlane) => ↑((1 / ⟨z.im, ⋯⟩) ^ 2)
source
instance UpperHalfPlane.instIsFiniteMeasureOnCompactsComapComplexCoeVolume :
MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
source
instance UpperHalfPlane.instIsLocallyFiniteMeasureComapComplexCoeVolume :
MeasureTheory.IsLocallyFiniteMeasure (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
source
instance UpperHalfPlane.instSigmaFiniteComapComplexCoeVolume :
MeasureTheory.SigmaFinite (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
source
instance UpperHalfPlane.instSFiniteComapComplexCoeVolume :
MeasureTheory.SFinite (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
source
instance UpperHalfPlane.instIsLocallyFiniteMeasureVolume :
MeasureTheory.IsLocallyFiniteMeasure MeasureTheory.volume
source
instance UpperHalfPlane.instIsFiniteMeasureOnCompactsVolume :
MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume
source
instance UpperHalfPlane.instSigmaFiniteVolume :
MeasureTheory.SigmaFinite MeasureTheory.volume
source
instance UpperHalfPlane.instSFiniteVolume :
MeasureTheory.SFinite MeasureTheory.volume
source
theorem UpperHalfPlane.volume_eq_lintegral (s : Set UpperHalfPlane) :
MeasureTheory.volume s = ∫⁻ (z : ℂ) in UpperHalfPlane.coe '' s, ↑((1 / ‖z.im‖₊) ^ 2)

Express the volume of a measurable set as a Lebesgue integral over the corresponding subset of ℂ.

source
instance UpperHalfPlane.instSMulInvariantMeasureGeneralLinearGroupFinOfNatNatRealVolume :
MeasureTheory.SMulInvariantMeasure (GL (Fin 2) ℝ) UpperHalfPlane MeasureTheory.volume

The measure on the upper half-plane is invariant under GL(2, ℝ).