English
If μ is finite, G is countable, and s is measurable, along with quasi-measure-preserving properties and an upper bound μ(univ) ≤ ∑ μ(g•s), then s is a fundamental domain.
Русский
Пусть μ — конечная мера, G счётно, s измерима, и выполняются условия квази-изменения меры и верхняя граница μ(всё) ≤ ∑ μ(g•s). Тогда s является фундаментальной доменной областью.
LaTeX
$$$\\text{IsFiniteMeasure}(μ) \\land \\text{Countable}(G) \\rightarrow (h\\; s \\; μ) \\Rightarrow \\text{IsFundamentalDomain}(G,s,μ)$$$
Lean4
/-- If a measurable space has a finite measure `μ` and a countable group `G` acts
quasi-measure-preservingly, then to show that a set `s` is a fundamental domain, it is sufficient
to check that its translates `g • s` are (almost) disjoint and that the sum `∑' g, μ (g • s)` is
sufficiently large. -/
@[to_additive /-- If a measurable space has a finite measure `μ` and a countable additive group `G` acts
quasi-measure-preservingly, then to show that a set `s` is a fundamental domain, it is sufficient
to check that its translates `g +ᵥ s` are (almost) disjoint and that the sum `∑' g, μ (g +ᵥ s)` is
sufficiently large. -/
]
theorem mk_of_measure_univ_le [IsFiniteMeasure μ] [Countable G] (h_meas : NullMeasurableSet s μ)
(h_ae_disjoint : ∀ g ≠ (1 : G), AEDisjoint μ (g • s) s)
(h_qmp : ∀ g : G, QuasiMeasurePreserving (g • · : α → α) μ μ)
(h_measure_univ_le : μ (univ : Set α) ≤ ∑' g : G, μ (g • s)) : IsFundamentalDomain G s μ :=
have aedisjoint : Pairwise (AEDisjoint μ on fun g : G => g • s) :=
pairwise_aedisjoint_of_aedisjoint_forall_ne_one h_ae_disjoint h_qmp
{ nullMeasurableSet := h_meas
aedisjoint
ae_covers :=
by
replace h_meas : ∀ g : G, NullMeasurableSet (g • s) μ := fun g => by rw [← inv_inv g, ← preimage_smul];
exact h_meas.preimage (h_qmp g⁻¹)
have h_meas' : NullMeasurableSet {a | ∃ g : G, g • a ∈ s} μ := by rw [← iUnion_smul_eq_setOf_exists];
exact .iUnion h_meas
rw [ae_iff_measure_eq h_meas', ← iUnion_smul_eq_setOf_exists]
refine le_antisymm (measure_mono <| subset_univ _) ?_
rw [measure_iUnion₀ aedisjoint h_meas]
exact h_measure_univ_le }
