setLIntegral_eq_tsum — Mathlib

English

For any t ⊆ α, the lintegral over t equals the sum over G of the lintegrals over t ∩ g•s: ∫⁻ x in t, f x ∂μ = ∑' g : G ∫⁻ x in t ∩ g • s, f x ∂μ.

Русский

Для любого множества t ⊆ α линегральная по t равна сумме по g∈G линегралов по t ∩ g•s: ∫⁻ 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 \\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 t ∩ g • s, f x ∂μ :=
  calc
    ∫⁻ x in t, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂μ.restrict t :=
      h.lintegral_eq_tsum_of_ac restrict_le_self.absolutelyContinuous _
    _ = ∑' g : G, ∫⁻ x in t ∩ g • s, f x ∂μ := by simp only [h.restrict_restrict, inter_comm]

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