English
Let a ∈ R be fixed. If f is integrable on every interval Ioc(a, b_i) with respect to μ, the real-valued sequence b_i tends to ∞ along l, and the integrals of ‖f‖ over these intervals are uniformly bounded by some I (i.e., eventually ≤ I), then f is integrable on the half-line Ioi(a) with respect to μ.
Русский
Пусть фиксировано a ∈ R. 如果 f интегрируема на каждом интервале Ioc(a, b_i) по μ, а последовательность b_i сходится к бесконечности по фильтру l и интегралы ‖f‖ по μ на интервала Ioc(a, b_i) ограничены сверху некоторой константой I, то f интегрируема на полполному интервале Ioi(a).
LaTeX
$$$\\Bigl(\\forall i,\\ IntegrableOn\\ f\\ (Ioc(a, b_i))\\ μ\\Bigr)\\to \\ Tendsto\\ b\\ l\\ atTop\\ Bigr)\\to \\Bigl(\\forall^{\\infty} i\\in l,\\ \\int x\\in a..b_i \\|f(x)\\|\\, \\partial μ \\le I\\Bigr)\\to \\ IntegrableOn\\ f\\ (Ioi\\ a)\\ μ.$$$
Lean4
theorem integrableOn_Ioi_of_intervalIntegral_norm_bounded (I a : ℝ) (hfi : ∀ i, IntegrableOn f (Ioc a (b i)) μ)
(hb : Tendsto b l atTop) (h : ∀ᶠ i in l, (∫ x in a..b i, ‖f x‖ ∂μ) ≤ I) : IntegrableOn f (Ioi a) μ :=
by
have hφ : AECover (μ.restrict <| Ioi a) l _ := aecover_Iic hb
have hfi : ∀ i, IntegrableOn f (Iic (b i)) (μ.restrict <| Ioi a) :=
by
intro i
rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
exact hfi i
refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)
filter_upwards [hb.eventually (eventually_ge_atTop a)] with i hbi
rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
exact id
