The invariant measure on ℍ and the Lebesgue measure on ℂ

Comparison of Mathlib's invariant measure volume : Measure ℍ (dx dy / y²) with the pullback of the Lebesgue measure along the embedding ℍ ↪ ℂ: the two are mutually absolutely continuous, since the density (Im τ)⁻² is everywhere positive. Consequently the invariant measure is positive on nonempty open sets, and preimages of Lebesgue-null subsets of ℂ are null in ℍ.

Main results

• UpperHalfPlane.volume_absolutelyContinuous_comap, UpperHalfPlane.comap_absolutelyContinuous_volume: mutual absolute continuity.
• the IsOpenPosMeasure instance for volume : Measure ℍ.
• UpperHalfPlane.volume_preimage_coe_null: preimages of Lebesgue-null sets are null.
• the NullSingletonClass instance for volume : Measure ℍ: points, hence countable sets, are null.
• UpperHalfPlane.volume_setOf_re_mem_Ico_and_lt_im: for A > 0, the region {a ≤ re z < b, A < im z} has invariant measure ENNReal.ofReal ((b - a) / A).

Split out of the Petersson inner-product development ported from the AINTLIB LeanModularForms project (https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms, Modularforms/PeterssonInnerProduct.lean, Chris Birkbeck).

instance UpperHalfPlane.instIsOpenPosMeasureComapComplexCoeVolume_tauCeti : (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume).IsOpenPosMeasure

The pullback of the Lebesgue measure along ℍ ↪ ℂ is positive on nonempty open sets.

theorem UpperHalfPlane.volume_absolutelyContinuous_comap : MeasureTheory.volume.AbsolutelyContinuous (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)

The invariant measure is absolutely continuous w.r.t. the pullback of the Lebesgue measure along ℍ ↪ ℂ.

theorem UpperHalfPlane.comap_absolutelyContinuous_volume : (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume).AbsolutelyContinuous MeasureTheory.volume

The pullback of the Lebesgue measure along ℍ ↪ ℂ is absolutely continuous w.r.t. the invariant measure, since the density (Im τ)⁻² is everywhere positive on ℍ.

instance UpperHalfPlane.instIsOpenPosMeasureVolume_tauCeti : MeasureTheory.volume.IsOpenPosMeasure

The invariant measure gives positive mass to nonempty open sets.

theorem UpperHalfPlane.volume_preimage_coe_null {S : Set ℂ} (hS : MeasureTheory.volume S = 0) : MeasureTheory.volume (UpperHalfPlane.coe ⁻¹' S) = 0

If a subset of ℂ has zero Lebesgue measure, its preimage in ℍ has zero invariant measure.

instance UpperHalfPlane.instNullSingletonClassVolume_tauCeti : MeasureTheory.NullSingletonClass MeasureTheory.volume

Points of ℍ have zero invariant measure.

theorem UpperHalfPlane.volume_setOf_re_mem_Ico_and_lt_im (a b : ℝ) {A : ℝ} (hA : 0 < A) : MeasureTheory.volume {z : UpperHalfPlane | z.re ∈ Set.Ico a b ∧ A < z.im} = ENNReal.ofReal ((b - a) / A)

The region of ℍ lying above the height A > 0 and over the interval [a, b) has invariant measure ENNReal.ofReal ((b - a) / A), which is zero when b ≤ a.