English
Under FTCFilter a l l' and appropriate hypotheses, the difference between the integral of f and the integral of c over moving intervals has a Little-o behavior relative to the measure of the interval, provided u ≤ᶠ v along the index.
Русский
При FTCFilter a l l' и разумных допущениях разность интегралов имеет поведение little-o по мере длины интервала, если u ≤ᶠ v.
LaTeX
$$$\\text{IsLittleO}_{lt}\\big( \\int_{u}^{v} f \\, dμ - \\int_{u}^{v} c \\, dμ \\big) \\text{ относит } ∫_{u}^{v} 1 \\, dμ$$$
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 ∂μ = μ (Ioc u v) • c + o(μ(Ioc u v))` as both `u` and `v` tend to `l`.
See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'` for a version that also works,
e.g., for `l = l' = Filter.atTop`. -/
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le [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 : u ≤ᶠ[lt] v) :
(fun t => (∫ x in u t..v t, f x ∂μ) - μ.real (Ioc (u t) (v t)) • c) =o[lt] fun t => μ.real (Ioc (u t) (v t)) :=
haveI := FTCFilter.meas_gen l
measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' hfm hf (FTCFilter.finiteAt_inner l) hu hv huv
