English
If s and t are fundamental domains for ν, then the pushforwards of μ restricted to s and t by π coincide: (μ|s).map π = (μ|t).map π.
Русский
Если s и t — фундаментальные области для ν, тогда отображения измерений по одинаковому проекции совпадают: (μ|s).map π = (μ|t).map π.
LaTeX
$$(μ|s).map π = (μ|t).map π$$
Lean4
@[to_additive]
theorem quotientMeasure_eq [Countable G] [MeasurableSpace G] {s t : Set α} [SMulInvariantMeasure G α μ]
[MeasurableSMul G α] (fund_dom_s : IsFundamentalDomain G s μ) (fund_dom_t : IsFundamentalDomain G t μ) :
(μ.restrict s).map π = (μ.restrict t).map π := by
ext U meas_U
rw [measure_map_restrict_apply (meas_U := meas_U), measure_map_restrict_apply (meas_U := meas_U)]
apply MeasureTheory.IsFundamentalDomain.measure_set_eq fund_dom_s fund_dom_t
· exact measurableSet_quotient.mp meas_U
· intro g
ext x
have : Quotient.mk α_mod_G (g • x) = Quotient.mk α_mod_G x :=
by
apply Quotient.sound
use g
simp only [mem_preimage, this]
