English
Let G act on α with an invariant measure μ and let s be a fundamental domain for this action. For any nonnegative function f: α → ℝ≥0∞, the integral of f over α with respect to μ equals the sum over G of the integrals of f over s after translating by g−1: ∫α f dμ = ∑g∈G ∫s f(g−1·x) dμ.
Русский
Пусть G действует на ℵ с сохраняемой мерой μ и пусть s — фундаментальная область для этого действия. Для любой неотрицательной функции f: ℵ → ℝ≥0∞ интеграл f по ℵ относительно μ равен сумме по g∈G интегралов f по s после смещения на g−1: ∫α f dμ = ∑g∈G ∫s f(g−1·x) dμ.
LaTeX
$$$$\\int_{\\alpha} f(x) \\, d\\mu(x) \\,=\\, \\sum_{g\\in G} \\int_{s} f(g^{-1} \\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) ∂μ :=
calc
∫⁻ x, f x ∂μ = ∑' g : G, ∫⁻ x in g • s, f x ∂μ := h.lintegral_eq_tsum f
_ = ∑' 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 =>
Eq.symm <| (measurePreserving_smul g⁻¹ μ).setLIntegral_comp_emb (measurableEmbedding_const_smul _) _ _
