English
Let I, a0, b0 ∈ R. If f is integrable on Ioc(a_i, b_i) for all i, a_i → a0, b_i → b0 along l, and ∫ x in Ioc(a_i, b_i) ‖f x‖ dμ are bounded by I along l, then f is integrable on Ioc(a0, b0).
Русский
Пусть I, a0, b0 ∈ R. Если f интегрируема на каждом Ioc(a_i, b_i) и a_i → a0, b_i → b0 по l, а интегралы ∥f∥ по μ на Ioc(a_i, b_i) ограничены сверху I по l, тогда f интегрируема на Ioc(a0, b0).
LaTeX
$$$\\{i\\}\\mapsto IntegrableOn\\ f\\ (Ioc(a_i, b_i))\\ μ\\quad ha: a_i\\to a_0,\\ hb: b_i\\to b_0,\\ h:\\forall^\\infty i,\\int x\\in Ioc(a_i,b_i)\\|f(x)\\|\\ μ ≤ I \\quad \\Longrightarrow\\quad IntegrableOn\\ f\\ (Ioc(a_0,b_0)).$$$
Lean4
theorem integrableOn_Ioc_of_intervalIntegral_norm_bounded {I a₀ b₀ : ℝ} (hfi : ∀ i, IntegrableOn f <| Ioc (a i) (b i))
(ha : Tendsto a l <| 𝓝 a₀) (hb : Tendsto b l <| 𝓝 b₀) (h : ∀ᶠ i in l, (∫ x in Ioc (a i) (b i), ‖f x‖) ≤ I) :
IntegrableOn f (Ioc a₀ b₀) :=
by
refine
(aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I (fun i => (hfi i).restrict) (h.mono fun i hi ↦ ?_)
rw [Measure.restrict_restrict measurableSet_Ioc]
grw [← hi]
gcongr
· apply ae_of_all
simp
· exact (hfi i).norm
· exact inter_subset_left
