English
For hs, the setIntegral over a sum of sets equals the sum of setLIntegral expressions, preserving invariance.
Русский
Для hs: интеграл по множеству через сумму множеств равен сумме соответствующих выражений интеграла над ограничениями.
LaTeX
$$$$\\text{setIntegral}_s(f) = \\sum_{g\\in G} \\text{setIntegral}_{(g\\cdot t)\\cap s}(f)$$$$
Lean4
@[to_additive]
theorem setIntegral_eq_tsum' (h : IsFundamentalDomain G s μ) {f : α → E} {t : Set α} (hf : IntegrableOn f t μ) :
∫ 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.setIntegral_eq_tsum hf
_ = ∑' 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 => (measurePreserving_smul g⁻¹ μ).setIntegral_image_emb (measurableEmbedding_const_smul _) _ _
