English
If hs and ht are fundamental domains, then the measures μs and μt coincide on all measurable sets A that respect G-invariance.
Русский
Если hs и ht — фундаментальные области, то меры μ|s и μ|t совпадают на всех измеримых множествах A, совместимых с инвариантностью по G.
LaTeX
$$$$\\mu|s = \\mu|t.$$$$
Lean4
@[to_additive]
protected theorem setIntegral_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) {f : α → E}
(hf : ∀ (g : G) (x), f (g • x) = f x) : ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ :=
by
by_cases hfs : IntegrableOn f s μ
· have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]
calc
∫ x in s, f x ∂μ = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ := ht.setIntegral_eq_tsum hfs
_ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
_ = ∫ x in t, f x ∂μ := (hs.setIntegral_eq_tsum' hft).symm
· rw [integral_undef hfs, integral_undef]
rwa [hs.integrableOn_iff ht hf] at hfs
