English
Let G be a group with a right-invariant measure μ and Γ a countable subgroup. Let 𝓕 be a fundamental domain for Γ and μ_𝓕 its restriction to 𝓕. Then the push-forward of μ to the quotient G/Γ is absolutely continuous with respect to the push-forward of μ restricted to 𝓕.
Русский
Пусть G — группа с правой инвариантной мерой μ, Γ — счётная подгруппа. Пусть 𝓕 — фундаментальная область для Γ, и μ_𝓕 — ограничение μ на 𝓕. Тогда переходная по фактору мера μ на тождественную пространство G/Γ абсолютно непрерывна по отношению к переходной мере μ_𝓕 на 𝓕.
LaTeX
$$$$\\operatorname{map} (\\mathrm{QuotientGroup.mk} : G \\to G ⧸ Γ) \\; μ \\ll \\operatorname{map} (\\mathrm{QuotientGroup.mk} : G \\to G ⧸ Γ) (μ \\restriction 𝓕).$$$$
Lean4
/-- Given a quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the restriction,
`μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
will take the value `∞` on any open set in the quotient! -/
@[to_additive /-- Given an additive quotient space `G ⧸ Γ` where `Γ` is `Countable`, and the
restriction, `μ_𝓕`, of a right-invariant measure `μ` on `G` to a fundamental domain `𝓕`, a set
in the quotient which has `μ_𝓕`-measure zero, also has measure zero under the
folding of `μ` under the quotient. Note that, if `Γ` is infinite, then the folded map
will take the value `∞` on any open set in the quotient! -/
]
theorem _root_.MeasureTheory.IsFundamentalDomain.absolutelyContinuous_map [μ.IsMulRightInvariant] :
map (QuotientGroup.mk : G → G ⧸ Γ) μ ≪ map (QuotientGroup.mk : G → G ⧸ Γ) (μ.restrict 𝓕) :=
by
set π : G → G ⧸ Γ := QuotientGroup.mk
have meas_π : Measurable π := continuous_quotient_mk'.measurable
apply AbsolutelyContinuous.mk
intro s s_meas hs
rw [map_apply meas_π s_meas] at hs ⊢
rw [Measure.restrict_apply] at hs
· apply h𝓕.measure_zero_of_invariant _ _ hs
intro γ
ext g
rw [Set.mem_smul_set_iff_inv_smul_mem, mem_preimage, mem_preimage]
congr! 1
convert QuotientGroup.mk_mul_of_mem g (γ⁻¹).2 using 1
exact MeasurableSet.preimage s_meas meas_π
