intervalIntegral_tendsto_integral_Ioi

English

For any a, if f is integrable on Ioi(a) and b_i → ∞, then ∫ x in a..b_i f x ∂μ tends to ∫ x in Ioi(a) f x ∂μ.

Русский

Для фиксированного a, если f интегрируема на (a, ∞) и b_i → ∞, то интеграл по [a, b_i] сходится к интегралу по (a, ∞).

LaTeX

$$$\\text{IntegrableOn}\\ f\\ μ\\ (Ioi\\ a)\\to\\ Tendsto\\ i\\mapsto ∫ x\\in a..b_i, f(x) ∂μ\\ l\\ (nhds\\ ∫ x\\in Ioi(a), f(x) ∂μ).$$$

Lean4

theorem intervalIntegral_tendsto_integral_Ioi (a : ℝ) (hfi : IntegrableOn f (Ioi a) μ) (hb : Tendsto b l atTop) :
    Tendsto (fun i => ∫ x in a..b i, f x ∂μ) l (𝓝 <| ∫ x in Ioi a, f x ∂μ) :=
  by
  let φ i := Iic (b i)
  have hφ : AECover (μ.restrict <| Ioi a) l φ := aecover_Iic hb
  refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_
  filter_upwards [hb.eventually (eventually_ge_atTop <| a)] with i hbi
  rw [intervalIntegral.integral_of_le hbi, Measure.restrict_restrict (hφ.measurableSet i), inter_comm]
  rfl

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