English
If a quotient measure μ satisfies QuotientMeasureEqMeasurePreimage with ν, and μ is finite, then the covolume of G acting on α with ν is finite.
Русский
Если μ удовлетворяет QuotientMeasureEqMeasurePreimage по ν и μ конечна, то ковольюм действия G на α по ν конечен.
LaTeX
$$$[QuotientMeasureEqMeasurePreimage\\nu\\mu] \\land [IsFiniteMeasure\\mu] \\Rightarrow covolume(G,\\alpha,\\nu) < \\infty.$$$
Lean4
/-- A finite measure `μ` on `α ⧸ G` satisfying `QuotientMeasureEqMeasurePreimage` has finite
covolume. -/
@[to_additive]
theorem covolume_ne_top (μ : Measure (Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage ν μ] [IsFiniteMeasure μ] :
covolume G α ν < ∞ := by
by_cases hasFun : HasFundamentalDomain G α ν
· obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
have H : μ univ < ∞ := IsFiniteMeasure.measure_univ_lt_top
rw [h𝓕.projection_respects_measure_apply (μ := μ) MeasurableSet.univ] at H
simpa [h𝓕.covolume_eq_volume ν] using H
· simp [covolume, hasFun]
