integrableOn_Ioc_of_intervalIntegral_norm_bounded_left

English

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

Русский

Если f интегрируема на Ioc(a_i, b) для всех i, a_i → a0, и интегралы по ‖f‖ на Ioc(a_i, b) верх bounded, то IntegrableOn f (Ioc(a0, b)).

LaTeX

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

Lean4

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

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