integrableOn_Ioc_of_intervalIntegral_norm_bounded_right

English

If f is integrable on Ioc(a, b_i) for all i, b_i → b0, and ∫ x in Ioc(a, b_i) ‖f x‖ ≤ I eventually, then IntegrableOn f (Ioc(a, b0)).

Русский

Если f интегрируема на Ioc(a, b_i) для всех i, b_i → b0, и интегралы ‖f‖ по μ на Ioc(a, b_i) ограничены сверху I, то IntegrableOn f (Ioc(a, b0)).

LaTeX

$$$\\bigl(\\forall i, IntegrableOn\\ f\\ (Ioc(a, b_i))\\ μ\\bigr)\\to \\ Tendsto\\ b\\ l (nhds\\ b_0)\\to \\ Tendsto\\ (\\int x\\in Ioc(a, b_i)\\|f(x)\\| ∂μ)\\ l\\ (nhds\\ I)\\to IntegrableOn\\ f\\ (Ioc(a, b_0)).$$$

Lean4

theorem integrableOn_Ioc_of_intervalIntegral_norm_bounded_right {I a b₀ : ℝ} (hfi : ∀ i, IntegrableOn f <| Ioc a (b i))
    (hb : Tendsto b l <| 𝓝 b₀) (h : ∀ᶠ i in l, (∫ x in Ioc a (b i), ‖f x‖) ≤ I) : IntegrableOn f (Ioc a b₀) :=
  integrableOn_Ioc_of_intervalIntegral_norm_bounded hfi tendsto_const_nhds hb h

Похожие утверждения