integral_eq_tsum' — Mathlib

English

For hs and ht, and any f, the integral equals the sum over G of the integral over the conjugate domain with f translated by g.

Русский

Для hs и ht интеграл равен сумме по g∈G интеграла по конголу домена с f, сдвинутой на g.

LaTeX

$$$$\\int f \\, d\\mu = \\sum_{g\\in G} \\int_{s} f(g^{-1} \\cdot x) \\, d\\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) ∂μ :=
  calc
    ∫ x, f x ∂μ = ∑' g : G, ∫ x in g • s, f x ∂μ := h.integral_eq_tsum f hf
    _ = ∑' g : G, ∫ x in g⁻¹ • s, f x ∂μ := ((Equiv.inv G).tsum_eq _).symm
    _ = ∑' g : G, ∫ x in s, f (g⁻¹ • x) ∂μ :=
      tsum_congr fun g => (measurePreserving_smul g⁻¹ μ).setIntegral_image_emb (measurableEmbedding_const_smul _) _ _

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