integrable_of_intervalIntegral_norm_bounded

English

If the interval integrals of ‖f‖ are bounded by I on left-bounded intervals and the left endpoint tends to -∞, then f is integrable on the interval starting at −∞ up to b.

Русский

Если интегралы ‖f‖ на левых интервалах ограничены и левая граница идёт к −∞, то f интегрируем на интервалы до b.

LaTeX

$$$IntegrableOn f (Iic b) μ$$$

Lean4

theorem integrable_of_intervalIntegral_norm_bounded (I : ℝ) (hfi : ∀ i, IntegrableOn f (Ioc (a i) (b i)) μ)
    (ha : Tendsto a l atBot) (hb : Tendsto b l atTop) (h : ∀ᶠ i in l, (∫ x in a i..b i, ‖f x‖ ∂μ) ≤ I) :
    Integrable f μ := by
  have hφ : AECover μ l _ := aecover_Ioc ha hb
  refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)
  filter_upwards [ha.eventually (eventually_le_atBot 0), hb.eventually (eventually_ge_atTop 0)] with i hai hbi ht
  rwa [← intervalIntegral.integral_of_le (hai.trans hbi)]

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