English
If f: β → α is a quasi-measure-preserving map and e: G → H is a bijection compatible with actions (Semiconj), then the preimage of a fundamental domain is a fundamental domain for the H-action w.r.t. ν.
Русский
Если f: β → α — квази-изменение меры, а e: G → H — биекция, совместимая по действиям, то предобраз фундаментальной области образует фундаментальную область для H‑действия по мере ν.
LaTeX
$$$\\text{IsFundamentalDomain}(H, f^{-1}(s), ν)$$$
Lean4
@[to_additive]
theorem preimage_of_equiv {ν : Measure β} (h : IsFundamentalDomain G s μ) {f : β → α}
(hf : QuasiMeasurePreserving f ν μ) {e : G → H} (he : Bijective e) (hef : ∀ g, Semiconj f (e g • ·) (g • ·)) :
IsFundamentalDomain H (f ⁻¹' s) ν
where
nullMeasurableSet := h.nullMeasurableSet.preimage hf
ae_covers := (hf.ae h.ae_covers).mono fun x ⟨g, hg⟩ => ⟨e g, by rwa [mem_preimage, hef g x]⟩
aedisjoint a b
hab := by
lift e to G ≃ H using he
have : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹ := by simp [hab]
have := (h.aedisjoint this).preimage hf
simp only [Semiconj] at hef
simpa only [onFun, ← preimage_smul_inv, preimage_preimage, ← hef, e.apply_symm_apply, inv_inv] using this
