English
Right-endpoint version: the difference between two interval integrals with right endpoint tends to a linear term in c with o-precision.
Русский
Правая граница: разность интегралов на интервале сходится к линейной части и имеет точность o.
LaTeX
$$$(∫_{a}^{v(t)} f - ∫_{a}^{u(t)} f) - ∫_{u(t)}^{v(t)} c = o( ∫_{u(t)}^{v(t)} 1 )$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict derivative in right endpoint for a locally finite
measure.
Let `f` be a measurable function integrable on `a..b`. Let `(lb, lb')` be a pair of
`intervalIntegral.FTCFilter`s around `b`. Suppose that `f` has a finite limit `c` at `lb' ⊓ ae μ`.
Then `∫ x in a..v, f x ∂μ - ∫ x in a..u, f x ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)` as
`u` and `v` tend to `lb`.
-/
theorem measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right (hab : IntervalIntegrable f μ a b)
(hmeas : StronglyMeasurableAtFilter f lb' μ) (hf : Tendsto f (lb' ⊓ ae μ) (𝓝 c)) (hu : Tendsto u lt lb)
(hv : Tendsto v lt lb) :
(fun t => ((∫ x in a..v t, f x ∂μ) - ∫ x in a..u t, f x ∂μ) - ∫ _ in u t..v t, c ∂μ) =o[lt] fun t =>
∫ _ in u t..v t, (1 : ℝ) ∂μ :=
by
simpa using
measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hab stronglyMeasurableAt_bot hmeas
((tendsto_bot : Tendsto _ ⊥ (𝓝 (0 : E))).mono_left inf_le_left) hf (tendsto_const_pure : Tendsto _ _ (pure a))
tendsto_const_pure hu hv
