English
If f is integrable on μ, and a_i ↓ atBot, b_i ↑ atTop, then the interval integrals ∫ f over [a_i, b_i] tend to ∫ f over ℝ (the whole line).
Русский
Если f интегрируемо по μ на всей прямой и интервалы [a_i, b_i] растягиваются на всю прямую, то интеграл сходится к интегралу по всей прямой.
LaTeX
$$$\\mathrm{IntegrableOn}\\ f\\ μ\\Rightarrow\\ Tendsto\\ (i\\mapsto ∫ x\\in a_i..b_i\\, f(x)\\, ∂μ)\\ l\\ (nhds\\ \\int x\\, f(x)\\, ∂μ).$$$
Lean4
theorem intervalIntegral_tendsto_integral (hfi : Integrable f μ) (ha : Tendsto a l atBot) (hb : Tendsto b l atTop) :
Tendsto (fun i => ∫ x in a i..b i, f x ∂μ) l (𝓝 <| ∫ x, f x ∂μ) :=
by
let φ i := Ioc (a i) (b i)
have hφ : AECover μ l φ := aecover_Ioc ha hb
refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_
filter_upwards [ha.eventually (eventually_le_atBot 0), hb.eventually (eventually_ge_atTop 0)] with i hai hbi
exact (intervalIntegral.integral_of_le (hai.trans hbi)).symm
