English
If the sets s_i are measurable, increase monotonically, and f is integrable over the union of all s_i, then the integrals over s_i converge to the integral over the union.
Русский
Если множества s_i измеримы и возрастают монотонно, а f интегрируема на объединении всех s_i, то интегралы по s_i сходятся к интегралу по объединению.
LaTeX
$$$$ \lim_{i \to \infty} \int_{x \in s_i} f(x) \, d\mu = \int_{x \in \bigcup_{n} s_n} f(x) \, d\mu $$$$
Lean4
theorem tendsto_setIntegral_of_monotone {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated]
{s : ι → Set X} (hsm : ∀ i, MeasurableSet (s i)) (h_mono : Monotone s) (hfi : IntegrableOn f (⋃ n, s n) μ) :
Tendsto (fun i => ∫ x in s i, f x ∂μ) atTop (𝓝 (∫ x in ⋃ n, s n, f x ∂μ)) :=
by
refine .of_neBot_imp fun hne ↦ ?_
have := (atTop_neBot_iff.mp hne).2
have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2
set S := ⋃ i, s i
have hSm : MeasurableSet S := MeasurableSet.iUnion_of_monotone h_mono hsm
have hsub {i} : s i ⊆ S := subset_iUnion s i
rw [← withDensity_apply _ hSm] at hfi'
set ν := μ.withDensity (‖f ·‖ₑ) with hν
refine Metric.nhds_basis_closedBall.tendsto_right_iff.2 fun ε ε0 => ?_
lift ε to ℝ≥0 using ε0.le
have : ∀ᶠ i in atTop, ν (s i) ∈ Icc (ν S - ε) (ν S + ε) :=
tendsto_measure_iUnion_atTop h_mono (ENNReal.Icc_mem_nhds hfi'.ne (ENNReal.coe_pos.2 ε0).ne')
filter_upwards [this] with i hi
rw [mem_closedBall_iff_norm', ← integral_diff (hsm i) hfi hsub, ← coe_nnnorm, NNReal.coe_le_coe, ← ENNReal.coe_le_coe]
refine (enorm_integral_le_lintegral_enorm _).trans ?_
rw [← withDensity_apply _ (hSm.diff (hsm _)), ← hν, measure_diff hsub (hsm _).nullMeasurableSet]
exacts [tsub_le_iff_tsub_le.mp hi.1, (hi.2.trans_lt <| ENNReal.add_lt_top.2 ⟨hfi', ENNReal.coe_lt_top⟩).ne]
