integrableOn_Iic_of_intervalIntegral_norm_bounded

English

If the limit of integrals exists and bounds are appropriate, then the full integral equals the limit integral.

Русский

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

LaTeX

$$$\\int f = \\lim_i \\int_{φ i} f$$$

Lean4

theorem integrableOn_Iic_of_intervalIntegral_norm_bounded (I b : ℝ) (hfi : ∀ i, IntegrableOn f (Ioc (a i) b) μ)
    (ha : Tendsto a l atBot) (h : ∀ᶠ i in l, (∫ x in a i..b, ‖f x‖ ∂μ) ≤ I) : IntegrableOn f (Iic b) μ :=
  by
  have hφ : AECover (μ.restrict <| Iic b) l _ := aecover_Ioi ha
  have hfi : ∀ i, IntegrableOn f (Ioi (a i)) (μ.restrict <| Iic b) :=
    by
    intro i
    rw [IntegrableOn, Measure.restrict_restrict (hφ.measurableSet i)]
    exact hfi i
  refine hφ.integrable_of_integral_norm_bounded I hfi (h.mp ?_)
  filter_upwards [ha.eventually (eventually_le_atBot b)] with i hai
  rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]
  exact id

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