English
Given a normal subgroup Γ of a topological group G with a fundamental domain 𝓕 of finite volume, the quotient map properly normalized satisfies QuotientMeasureEqMeasurePreimage.
Русский
Для нормальной подгруппы Γ нормального топологического множества G с конечным объемом фундаментальная область 𝓕; нормализованный отображение на т. к. фактор-группа удовлетворяет мерной предобразной связке.
LaTeX
$$$QuotientMeasureEqMeasurePreimage\nu\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_smulHaarMeasure {𝓕 : Set G} (h𝓕 : IsFundamentalDomain Γ.op 𝓕 ν)
(h𝓕_finite : ν 𝓕 ≠ ⊤) : QuotientMeasureEqMeasurePreimage ν ((ν ((π ⁻¹' (K : Set (G ⧸ Γ))) ∩ 𝓕)) • haarMeasure K) :=
by
set c := ν ((π ⁻¹' (K : Set (G ⧸ Γ))) ∩ 𝓕)
have c_ne_top : c ≠ ∞ := by
contrapose! h𝓕_finite
have : c ≤ ν 𝓕 := measure_mono (Set.inter_subset_right)
rw [h𝓕_finite] at this
exact top_unique this
set μ := c • haarMeasure K
have hμK : μ K = c := by simp [μ, haarMeasure_self]
haveI : SigmaFinite μ := by
clear_value c
lift c to NNReal using c_ne_top
exact SMul.sigmaFinite c
apply
IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure (h𝓕 := h𝓕) (meas_V := K.isCompact.measurableSet)
(μ := μ)
· exact K.interior_nonempty
· exact hμK
· rw [hμK]
exact c_ne_top
