English
If ν is sigma-finite and there exists a fundamental domain for the G-action, then the quotient measure μ defined via QuotientMeasureEqMeasurePreimage is sigma-finite.
Русский
Если ν сигма-конечна и существует фундаментальная область для действия G, то мера μ, заданная через QuotientMeasureEqMeasurePreimage, сигма-конечна.
LaTeX
$$$\\text{If }\\nu \\text{ is sigma-finite and a fundamental domain exists, then } μ \\text{ is sigma-finite for } ν.$$$
Lean4
/-- A measure `μ` on `α ⧸ G` satisfying `QuotientMeasureEqMeasurePreimage` and having finite
covolume is a finite measure. -/
@[to_additive]
theorem isFiniteMeasure_quotient (μ : Measure (Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage ν μ]
[hasFun : HasFundamentalDomain G α ν] (h : covolume G α ν ≠ ∞) : IsFiniteMeasure μ :=
by
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
rw [h𝓕.projection_respects_measure (μ := μ)]
have : Fact (ν 𝓕 < ∞) := by
apply Fact.mk
convert Ne.lt_top h
exact (h𝓕.covolume_eq_volume ν).symm
infer_instance
