lintegral_eq_tsum'' — Mathlib

English

Under the same setting, the lintegral of a nonnegative function equals the sum over G of the lintegrals over s after translating by g: ∫⁻ x f x ∂μ = ∑' g : G ∫⁻ x in s, f (g • x) ∂μ.

Русский

В той же постановке интеграл Лепега неотрицимой функции равен сумме по g∈G линегралов над s после переноса: ∫⁻ x f(x) dμ = ∑' g∈G ∫⁻ x∈s f(g•x) dμ.

LaTeX

$$$$\\int f \\, d\\mu = \\sum_{g\\in G} \\int_{s} f(g \\cdot x) \\, d\\mu(x).$$$$

Lean4

@[to_additive]
theorem lintegral_eq_tsum'' (h : IsFundamentalDomain G s μ) (f : α → ℝ≥0∞) :
    ∫⁻ x, f x ∂μ = ∑' g : G, ∫⁻ x in s, f (g • x) ∂μ :=
  (lintegral_eq_tsum' h f).trans ((Equiv.inv G).tsum_eq (fun g ↦ ∫⁻ (x : α) in s, f (g • x) ∂μ))

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