English
If h is a fundamental domain for G on α and t is any subset, then the decomposition with g⁻¹ on t yields ∫⁻ x in t, f x ∂μ = ∑' g ∫⁻ x in t ∩ g⁻¹•s, f x ∂μ.
Русский
Если h — фундаментальная область, то разложение по g⁻¹ по t даёт ∫⁻ x∈t f(x) dμ = ∑' g∈G ∫⁻ x∈t∩g⁻¹•s f(x) dμ.
LaTeX
$$$$\\int_{t} f \\, d\\mu \\,=\\, \\sum_{g\\in G} \\int_{t \\cap g^{-1} \\cdot s} f \\, d\\mu.$$$$
Lean4
@[to_additive]
theorem setLIntegral_eq_tsum' (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0∞) (t : Set α) :
∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :=
calc
∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ := h.setLIntegral_eq_tsum f t
_ = ∑' g : G, ∫⁻ x in t ∩ g⁻¹ • s, f x ∂μ := ((Equiv.inv G).tsum_eq _).symm
_ = ∑' g : G, ∫⁻ x in g⁻¹ • (g • t ∩ s), f x ∂μ := by simp only [smul_set_inter, inv_smul_smul]
_ = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ :=
tsum_congr fun g =>
Eq.symm <| (measurePreserving_smul g⁻¹ μ).setLIntegral_comp_emb (measurableEmbedding_const_smul _) _ _
