setLIntegral_eq — Mathlib

English

For h and t, the restricted integral over t of f equals the sum over g of the restricted integral over t ∩ g•s of f translated by g⁻¹.

Русский

Для h и t интеграл по t с ограничением равен сумме по g от ограниченного интеграла по t ∩ g•s с преобразованием f г⁻¹.

LaTeX

$$$$\\int_{t} f\, d\\mu \\,=\\, \\sum_{g\\in G} \\int_{t \\cap (g \\cdot s)} f(g^{-1} \\cdot x) \\, d\\mu(x).$$$$

Lean4

@[to_additive]
protected theorem setLIntegral_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) (f : α → ℝ≥0∞)
    (hf : ∀ (g : G) (x), f (g • x) = f x) : ∫⁻ x in s, f x ∂μ = ∫⁻ x in t, f x ∂μ :=
  calc
    ∫⁻ x in s, f x ∂μ = ∑' g : G, ∫⁻ x in s ∩ g • t, f x ∂μ := ht.setLIntegral_eq_tsum _ _
    _ = ∑' g : G, ∫⁻ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
    _ = ∫⁻ x in t, f x ∂μ := (hs.setLIntegral_eq_tsum' _ _).symm

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