English
For any b, if f integrable on Iic(b) and a_i ↓ atBot, then ∫ x in a_i..b f x ∂μ tends to ∫ x in Iic(b) f x ∂μ.
Русский
Пусть для любого b функция f интегрируема на Iic(b); при этом a_i сходится к −∞; тогда интеграл по интервалу [a_i, b] сходится к интегралу по (-∞, b].
LaTeX
$$$\\text{IntegrableOn}\\ f\\ μ\\ (Iic\\ b)\\to\\ Tendsto\\ i\\mapsto ∫ x\\in a_i..b, f(x) ∂μ\\ l\\ (nhds\\ ∫ x\\in Iic(b), f(x) ∂μ).$$$
Lean4
theorem intervalIntegral_tendsto_integral_Iic (b : ℝ) (hfi : IntegrableOn f (Iic b) μ) (ha : Tendsto a l atBot) :
Tendsto (fun i => ∫ x in a i..b, f x ∂μ) l (𝓝 <| ∫ x in Iic b, f x ∂μ) :=
by
let φ i := Ioi (a i)
have hφ : AECover (μ.restrict <| Iic b) l φ := aecover_Ioi ha
refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_
filter_upwards [ha.eventually (eventually_le_atBot <| b)] with i hai
rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]
rfl
