English
If f is integrable on all Ioc(a, b_i) with b_i → ∞, and the norms ∫_a^{b_i} ‖f‖ converge along l to a finite limit I, then f is integrable on Ioi(a).
Русский
Пусть f интегрируема на каждом Ioc(a, b_i) с b_i → ∞, и интегралы норм ∥f∥ сходятся к конечному пределу I по l; тогда f интегрируема на Ioi(a).
LaTeX
$$$\\Bigl(\\forall i,\\ IntegrableOn\\ f\\ (Ioc(a, b_i))\\ μ\\Bigr)\\to \\ Tendsto\\ b\\ l\\ atTop\\ Bigr)\\to \\ Tendsto\\ (\\lambda i,\\int x\\in a..b_i\\|f(x)\\|\\, ∂μ)\\ l\\ (𝓝\\ I)\\to \\ IntegrableOn\\ f\\ (Ioi\\ a)\\ μ.$$$
Lean4
/-- If `f` is integrable on intervals `Ioc a (b i)`,
where `b i` tends to ∞, and
`∫ x in a .. b i, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`,
then `f` is integrable on the interval (a, ∞) -/
theorem integrableOn_Ioi_of_intervalIntegral_norm_tendsto (I a : ℝ) (hfi : ∀ i, IntegrableOn f (Ioc a (b i)) μ)
(hb : Tendsto b l atTop) (h : Tendsto (fun i => ∫ x in a..b i, ‖f x‖ ∂μ) l (𝓝 <| I)) : IntegrableOn f (Ioi a) μ :=
let ⟨I', hI'⟩ := h.isBoundedUnder_le
integrableOn_Ioi_of_intervalIntegral_norm_bounded I' a hfi hb hI'
