English
For a fundamental domain 𝓕 and any measurable g on G/Γ, the essSup of g over μ_𝓕 equals the essSup of g composed with the quotient map over μ.
Русский
Для фундаментальной области 𝓕 и любого измеримого g на G/Γ essSup g по мере μ_𝓕 равен essSup от g(множество через тождественный отображение по кварте μ.
LaTeX
$$$essSup\, g\, (\mu_{\mathcal{F}}) = essSup\, (g\circ (QuotientGroup.mk))\, \mu$$$
Lean4
/-- The `essSup` of a function `g` on the quotient space `G ⧸ Γ` with respect to the pushforward
of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental domain `𝓕`, is the
same as the `essSup` of `g`'s lift to the universal cover `G` with respect to `μ`. -/
@[to_additive /-- The `essSup` of a function `g` on the additive quotient space `G ⧸ Γ` with respect
to the pushforward of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental
domain `𝓕`, is the same as the `essSup` of `g`'s lift to the universal cover `G` with respect
to `μ`. -/
]
theorem essSup_comp_quotientGroup_mk [μ.IsMulRightInvariant] {g : G ⧸ Γ → ℝ≥0∞} (g_ae_measurable : AEMeasurable g μ_𝓕) :
essSup g μ_𝓕 = essSup (fun (x : G) ↦ g x) μ :=
by
have hπ : Measurable (QuotientGroup.mk : G → G ⧸ Γ) := continuous_quotient_mk'.measurable
rw [essSup_map_measure g_ae_measurable hπ.aemeasurable]
refine h𝓕.essSup_measure_restrict ?_
intro ⟨γ, hγ⟩ x
dsimp
congr 1
exact QuotientGroup.mk_mul_of_mem x hγ
