hasSum_lintegral_measure — Mathlib

English

The series of numbers ∫ f dμ_i has a HasSum equal to ∫ f d(Measure.sum μ).

Русский

Задаёт равенство HasSum для ряда интегралов: сумма линеинтегралов равна интегралу по сумме мер.

LaTeX

$$$\\text{HasSum} \\bigl( i \\mapsto \\int f \\, d\\mu_i \\bigr) \\bigm| (\\int f \\, d(\\sum_i \\mu_i))$$$

Lean4

theorem hasSum_lintegral_measure {ι} {_ : MeasurableSpace α} (f : α → ℝ≥0∞) (μ : ι → Measure α) :
    HasSum (fun i => ∫⁻ a, f a ∂μ i) (∫⁻ a, f a ∂Measure.sum μ) :=
  (lintegral_sum_measure f μ).symm ▸ ENNReal.summable.hasSum

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