integral_eq_tsum'' — Mathlib

English

If G is a group acting on α with invariant measure μ and s is a fundamental domain, then the integral of f over α equals the sum over G of the integral over g•s of f restricted by g, adjusting by measure-preserving transform.

Русский

Если G действует на α с инвариантной мерой μ и s — фундаментальная область, то интеграл по α равен сумме по g∈G интегралов по g•s с учетом преобразований, сохраняющих меру.

LaTeX

$$$$\\int_{\\alpha} f(x) \\partial\\mu(x) = \\sum_{g\\in G} \\int_{g \\cdot s} f(x) \\partial\\mu(x).$$$$

Lean4

@[to_additive]
theorem integral_eq_tsum'' (h : IsFundamentalDomain G s μ) (f : α → E) (hf : Integrable f μ) :
    ∫ x, f x ∂μ = ∑' g : G, ∫ x in s, f (g • x) ∂μ :=
  (integral_eq_tsum' h f hf).trans ((Equiv.inv G).tsum_eq (fun g ↦ ∫ (x : α) in s, f (g • x) ∂μ))

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