lintegral_eq_tsum_of_ac — Mathlib

English

For a fundamental domain G and ν ≪ μ, and f: α → ℝ≥0∞, the lintegral of f with respect to ν equals the tsum over g of the lintegral of f over g • s with respect to ν.

Русский

Для фундаментальной области G и ν ≪ μ, при f: α → ℝ≥0∞ выполняется: ∫ f dν = ∑' g ∫ f над g•s dν.

LaTeX

$$$\\int f \\, d\\nu = \\sum_{g\\in G} \\int_{g\\cdot s} f \\, d\\nu$$$

Lean4

@[to_additive]
theorem lintegral_eq_tsum_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) (f : α → ℝ≥0∞) :
    ∫⁻ x, f x ∂ν = ∑' g : G, ∫⁻ x in g • s, f x ∂ν := by rw [← lintegral_sum_measure, h.sum_restrict_of_ac hν]

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