English
A general FTC-1 style result: the difference between two interval integrals minus the corresponding constant-integral difference is little-o of the interval length, under suitable hypotheses.
Русский
Общее утверждение FTC-1: разность интегралов минус соответствующая константа имеет поведение little-o относительно длины интервала.
LaTeX
$$$(∫_{va}^{vb} f) - (∫_{ua}^{ub} f) - ((∫_{ub}^{vb} c) - (∫_{ua}^{va} c)) = o( ||∫_{ua}^{va} 1|| + ||∫_{ub}^{vb} 1|| )$$$
Lean4
/-- **Fundamental theorem of calculus-1**, local version.
If `f` has a finite limit `c` almost surely at `l'`, where `(l, l')` is an
`intervalIntegral.FTCFilter` pair around `a`, then `∫ x in u..v, f x ∂μ = (v - u) • c + o (v - u)`
as both `u` and `v` tend to `l`. -/
theorem integral_sub_linear_isLittleO_of_tendsto_ae [FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l')
(hf : Tendsto f (l' ⊓ ae volume) (𝓝 c)) {u v : ι → ℝ} (hu : Tendsto u lt l) (hv : Tendsto v lt l) :
(fun t => (∫ x in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u) := by
simpa [integral_const] using measure_integral_sub_linear_isLittleO_of_tendsto_ae hfm hf hu hv
