setIntegral_eq_tsum — Mathlib

English

If hs and ht are fundamental domains and f is invariant, then the restricted integrals over s and t are equal when integrated with the same f.

Русский

Если hs и ht — фундаментальные домены и f инвариантна, то ограниченные интегралы по s и t равны.

LaTeX

$$$$\\int_{s} f \\, d\\mu = \\int_{t} f \\, d\\mu.$$$$

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 t ∩ g • s, f x ∂μ :=
  calc
    ∫ x in t, f x ∂μ = ∑' g : G, ∫ x in g • s, f x ∂μ.restrict t :=
      h.integral_eq_tsum_of_ac restrict_le_self.absolutelyContinuous f hf
    _ = ∑' g : G, ∫ x in t ∩ g • s, f x ∂μ := by simp only [h.restrict_restrict, inter_comm]

Похожие утверждения