English
Under appropriate hypotheses, the difference between the right-hand and left-hand interval integrals behaves like a linear term in (v-u) with a small-o remainder as u,v approach the limit along the filter.
Русский
При подходящих гипотезах разность правой и левой частей интеграла по переменным диапазона ведет себя как линейная функция от (v-u) с остатком из little-o при стремлении u,v вдоль фильтра.
LaTeX
$$$(\\text{hab}) \\to (\\text{hmeas}) \\to (\\text{hf}) \\to (\\text{hu}) \\to (\\text{hv}) \\,:\; \\left( (\\int_{a}^{v} f) - (\\int_{a}^{u} f) - (v-u)\\, c \\right) = o_{lt}(v-u).$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability at filter in both endpoints.
If `f` is a measurable function integrable on `a..b`, `(lb, lb')` is an `intervalIntegral.FTCFilter`
pair around `b`, and `f` has a finite limit `c` almost surely at `lb'`, then
`(∫ x in a..v, f x) - ∫ x in a..u, f x = (v - u) • c + o(‖v - u‖)` as `u` and `v` tend to `lb`.
This lemma could've been formulated using `HasStrictDerivAtFilter` if we had this definition. -/
theorem integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right (hab : IntervalIntegrable f volume a b)
(hmeas : StronglyMeasurableAtFilter f lb') (hf : Tendsto f (lb' ⊓ ae volume) (𝓝 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) - (v t - u t) • c) =o[lt] (v - u) :=
by
simpa only [integral_const, smul_eq_mul, mul_one] using
measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hab hmeas hf hu hv
