hasSum_integral_iUnion — Mathlib

English

If s_i are measurable, pairwise disjoint, and f is integrable on their union, then HasSum of the series of integrals equals the integral over the union.

Русский

Если множества s_i измеримы, попарно непересекаются, и f интегрируема на их объединении, то сумма рядов интегралов равна интегралу по объединению.

LaTeX

$$$$ \text{HasSum}\left( n \mapsto \int_{x \in s_n} f(x) \, d\mu \right) \;=\; \int_{x \in \bigcup_n s_n} f(x) \, d\mu $$$$

Lean4

theorem hasSum_integral_iUnion {ι : Type*} [Countable ι] {s : ι → Set X} (hm : ∀ i, MeasurableSet (s i))
    (hd : Pairwise (Disjoint on s)) (hfi : IntegrableOn f (⋃ i, s i) μ) :
    HasSum (fun n => ∫ x in s n, f x ∂μ) (∫ x in ⋃ n, s n, f x ∂μ) :=
  hasSum_integral_iUnion_ae (fun i => (hm i).nullMeasurableSet) (hd.mono fun _ _ h => h.aedisjoint) hfi

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