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, ℝ).
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
The invariant measure on the upper half-plane, defined by dx dy / y ^ 2.
theorem
UpperHalfPlane.volume_def :
MeasureTheory.volume = (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume).withDensity fun (z : UpperHalfPlane) =>
↑((1 / ⟨z.im, ⋯⟩) ^ 2)
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 ℂ.
The measure on the upper half-plane is invariant under GL(2, ℝ).