integrable_of_intervalIntegral_norm_tendsto

English

If f is integrable on Ioc(a_i)(b_i) with a_i → -∞ and Tendsto of interval norms exists, then integrable on Icc-like interval.

Русский

Если f интегрируем на Ioc(a_i)(b_i) и предел норм интервалов существует, то интегрируемость на ограниченных пределах сохраняется.

LaTeX

$$$Integrable f μ$$$

Lean4

/-- If `f` is integrable on intervals `Ioc (a i) (b i)`,
where `a i` tends to -∞ and `b i` tends to ∞, and
`∫ x in a i .. b i, ‖f x‖ ∂μ` converges to `I : ℝ` along a filter `l`,
then `f` is integrable on the interval (-∞, ∞) -/
theorem integrable_of_intervalIntegral_norm_tendsto (I : ℝ) (hfi : ∀ i, IntegrableOn f (Ioc (a i) (b i)) μ)
    (ha : Tendsto a l atBot) (hb : Tendsto b l atTop) (h : Tendsto (fun i => ∫ x in a i..b i, ‖f x‖ ∂μ) l (𝓝 I)) :
    Integrable f μ :=
  let ⟨I', hI'⟩ := h.isBoundedUnder_le
  integrable_of_intervalIntegral_norm_bounded I' hfi ha hb hI'

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