English
If upstairs ν is sigma-finite and there is a fundamental domain, then the quotient measure μ on α/G satisfying QuotientMeasureEqMeasurePreimage is sigma-finite.
Русский
Если верхняя мера ν сигма- فعинитна и существует фундаментальная область, то мера μ на α/G, удовлетворяющая QuotientMeasureEqMeasurePreimage, сигма-вещественна.
LaTeX
$$$[i: SigmaFinite ν][i': HasFundamentalDomain G α ν] (μ : Measure(Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage ν μ] : SigmaFinite μ.$$$
Lean4
/-- If a measure `μ` on a quotient satisfies `QuotientMeasureEqMeasurePreimage` with respect to a
sigma-finite measure `ν`, then it is itself `SigmaFinite`. -/
@[to_additive]
theorem sigmaFiniteQuotient [i : SigmaFinite ν] [i' : HasFundamentalDomain G α ν] (μ : Measure (Quotient α_mod_G))
[QuotientMeasureEqMeasurePreimage ν μ] : SigmaFinite μ :=
by
rw [sigmaFinite_iff]
obtain ⟨A, hA_meas, hA, hA'⟩ := Measure.toFiniteSpanningSetsIn (h := i)
simp only [mem_setOf_eq] at hA_meas
refine ⟨⟨fun n ↦ π '' (A n), by simp, fun n ↦ ?_, ?_⟩⟩
· obtain ⟨s, fund_dom_s⟩ := i'
have : π ⁻¹' (π '' (A n)) = _ := MulAction.quotient_preimage_image_eq_union_mul (A n) (G := G)
have measπAn : MeasurableSet (π '' A n) := by
let _ : Setoid α := α_mod_G
rw [measurableSet_quotient, Quotient.mk''_eq_mk, this]
apply MeasurableSet.iUnion
exact fun g ↦ MeasurableSet.const_smul (hA_meas n) g
rw [fund_dom_s.projection_respects_measure_apply (μ := μ) measπAn, this, iUnion_inter]
refine lt_of_le_of_lt ?_ (hA n)
rw [fund_dom_s.measure_eq_tsum (A n)]
exact measure_iUnion_le _
· rw [← image_iUnion, hA']
refine image_univ_of_surjective (by convert Quotient.mk'_surjective)
