English
The essSup on the quotient by a subgroup Γ equals the essSup of the lift to the covering group with respect to the pushforward measure.
Русский
Предел essSup на фактор-пространстве по подгруппе Γ равен пределу essSup подъема-распределения в покрывающем группе по отношению к отображению-переносу.
LaTeX
$$$essSup\, g\;\mu_{\mathcal{F}} = essSup\, (g\circ π)\;\mu$$$
Lean4
/-- Given a normal subgroup `Γ` of a topological group `G` with Haar measure `μ`, which is also
right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
properly normalized, satisfies `QuotientMeasureEqMeasurePreimage`. -/
@[to_additive /-- Given a normal
subgroup `Γ` of an additive topological group `G` with Haar measure `μ`, which is also
right-invariant, and a finite volume fundamental domain `𝓕`, the quotient map to `G ⧸ Γ`,
properly normalized, satisfies `AddQuotientMeasureEqMeasurePreimage`. -/
]
theorem QuotientMeasureEqMeasurePreimage_HaarMeasure {𝓕 : Set G} (h𝓕 : IsFundamentalDomain Γ.op 𝓕 ν)
[IsMulLeftInvariant μ] [SigmaFinite μ] {V : Set (G ⧸ Γ)} (hV : (interior V).Nonempty) (meas_V : MeasurableSet V)
(hμK : μ V = ν ((π ⁻¹' V) ∩ 𝓕)) (neTopV : μ V ≠ ⊤) : QuotientMeasureEqMeasurePreimage ν μ :=
by
apply IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := h𝓕) (meas_V := meas_V)
· rw [hμK]
intro c_eq_zero
apply IsOpenPosMeasure.open_pos (interior (π ⁻¹' V)) (μ := ν)
· simp
· apply Set.Nonempty.mono (preimage_interior_subset_interior_preimage continuous_coinduced_rng)
apply hV.preimage'
simp
· apply measure_mono_null (h := interior_subset)
apply h𝓕.measure_zero_of_invariant (ht := fun g ↦ QuotientGroup.sound _ _ g)
exact c_eq_zero
· exact hμK
· exact neTopV
