English
The quotient map π preserves the measure when restricted to a fundamental domain, mapping the upstairs restricted volume ν|𝓕 to the downstairs quotient measure μ that satisfies quotient-preimage relations.
Русский
Квотиентный отображатель π сохраняет меру при ограничении на фундаментальную область, переводя меру ν|𝓕 в меру μ на факторпространстве так, что выполняются условия QuotientMeasureEqMeasurePreimage.
LaTeX
$$$\\operatorname{MeasurePreserving}(\\\\pi, \\\\nu|_{\\\\mathcal{F}}, \\\\mu).$$$
Lean4
/-- The quotient map to `α ⧸ G` is measure-preserving between the restriction of `volume` to a
fundamental domain in `α` and a related measure satisfying `QuotientMeasureEqMeasurePreimage`. -/
@[to_additive IsAddFundamentalDomain.measurePreserving_add_quotient_mk]
theorem measurePreserving_quotient_mk {𝓕 : Set α} (h𝓕 : IsFundamentalDomain G 𝓕 ν) (μ : Measure (Quotient α_mod_G))
[QuotientMeasureEqMeasurePreimage ν μ] : MeasurePreserving π (ν.restrict 𝓕) μ
where
measurable := measurable_quotient_mk' (s := α_mod_G)
map_eq := by
haveI : HasFundamentalDomain G α ν := ⟨𝓕, h𝓕⟩
rw [h𝓕.projection_respects_measure (μ := μ)]
