English
If s is a fundamental domain for G with respect to ν, then covolume G α ν equals the ν-measure of s.
Русский
Если s — фундаментальная область для G относительно ν, то ковольюм равен мере ν от s.
LaTeX
$$\\mathrm{covolume}(G,\\alpha,ν) = ν(s)$$
Lean4
protected theorem fundamentalInterior : IsFundamentalDomain G (fundamentalInterior G s) μ
where
nullMeasurableSet := hs.nullMeasurableSet.fundamentalInterior _ _
ae_covers :=
by
simp_rw [ae_iff, not_exists, ← mem_inv_smul_set_iff, setOf_forall, ← compl_setOf, setOf_mem_eq, ← compl_iUnion]
have : ((⋃ g : G, g⁻¹ • s) \ ⋃ g : G, g⁻¹ • fundamentalFrontier G s) ⊆ ⋃ g : G, g⁻¹ • fundamentalInterior G s := by
simp_rw [diff_subset_iff, ← iUnion_union_distrib, ← smul_set_union (α := G) (β := α),
fundamentalFrontier_union_fundamentalInterior];
rfl
refine eq_bot_mono (μ.mono <| compl_subset_compl.2 this) ?_
simp only [iUnion_inv_smul, compl_sdiff, ENNReal.bot_eq_zero, himp_eq, sup_eq_union,
@iUnion_smul_eq_setOf_exists _ _ _ _ s]
exact
measure_union_null (measure_iUnion_null fun _ => measure_smul_null hs.measure_fundamentalFrontier _) hs.ae_covers
aedisjoint := (pairwise_disjoint_fundamentalInterior _ _).mono fun _ _ => Disjoint.aedisjoint
