English
A dual formulation: if v tends to a and u tends to a with v ≥ᶠ u along lt, then the corresponding Little-o statement holds in the dual orientation.
Русский
Двойная формулировка: если v тяготеет к a и u тяготеет к a с условием v ≥ᶠ u, то выполняется соответствующее little-o.
LaTeX
$$$\\text{IsLittleO}_{lt}( \\text{some difference}, \\ a) $$$
Lean4
/-- **Fundamental theorem of calculus-1**, local version for any measure.
Let filters `l` and `l'` be related by `[intervalIntegral.FTCFilter a l l']`; let `μ` be a locally
finite measure. If `f` has a finite limit `c` at `l' ⊓ ae μ`, then
`∫ x in u..v, f x ∂μ = -μ (Set.Ioc v u) • c + o(μ(Set.Ioc v u))` as both `u` and `v` tend to `l`.
See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge'` for a version that also works,
e.g., for `l = l' = Filter.atTop`. -/
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge [CompleteSpace E] [FTCFilter a l l']
(hfm : StronglyMeasurableAtFilter f l' μ) (hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)) (hu : Tendsto u lt l)
(hv : Tendsto v lt l) (huv : v ≤ᶠ[lt] u) :
(fun t => (∫ x in u t..v t, f x ∂μ) + μ.real (Ioc (v t) (u t)) • c) =o[lt] fun t => μ.real (Ioc (v t) (u t)) :=
haveI := FTCFilter.meas_gen l
measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' hfm hf (FTCFilter.finiteAt_inner l) hu hv huv
