English
If s is measurable, there is a condition on almost-everywhere translates and quasi-measure-preserving maps that yields IsFundamentalDomain G s μ.
Русский
Если s измеримо и выполняются условия AE-покрытия и квази-изменения меры по переносу, то s является фундаментальной доменной областью.
LaTeX
$$$\\text{IsFundamentalDomain}(G,s,μ)$$$
Lean4
/-- For `s` to be a fundamental domain, it's enough to check
`MeasureTheory.AEDisjoint (g • s) s` for `g ≠ 1`. -/
@[to_additive /-- For `s` to be a fundamental domain, it's enough to check
`MeasureTheory.AEDisjoint (g +ᵥ s) s` for `g ≠ 0`. -/
]
theorem mk'' (h_meas : NullMeasurableSet s μ) (h_ae_covers : ∀ᵐ x ∂μ, ∃ g : G, g • x ∈ s)
(h_ae_disjoint : ∀ g, g ≠ (1 : G) → AEDisjoint μ (g • s) s)
(h_qmp : ∀ g : G, QuasiMeasurePreserving ((g • ·) : α → α) μ μ) : IsFundamentalDomain G s μ
where
nullMeasurableSet := h_meas
ae_covers := h_ae_covers
aedisjoint := pairwise_aedisjoint_of_aedisjoint_forall_ne_one h_ae_disjoint h_qmp
