integrableOn_Iic_of_intervalIntegral_norm_tendsto

English

If the average of the norm over expanding intervals converges to a limit, then f is integrable on the whole line.

Русский

Если среднее по норме на растущих интервалах сходится к пределу, то f интегрируем на всей прямой.

LaTeX

$$$Integrable f μ$$$

Lean4

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

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