English
There is a standard FTCFilter nhds that links a real number a with its neighborhood filter in a compatibility fashion.
Русский
Стандартная связка nhds образует совместимый FTCFilter вокруг a.
LaTeX
$$$\\mathrm{FTCFilter}(a, \\mathcal{N}(a), \\mathcal{N}(a))$$$
Lean4
/-- **Fundamental theorem of calculus-1**, local version for any measure.
Let filters `l` and `l'` be related by `TendstoIxxClass Ioc`.
If `f` has a finite limit `c` at `l ⊓ ae μ`, where `μ` is a measure
finite at `l`, then `∫ x in u..v, f x ∂μ = -μ (Ioc v u) • c + o(μ(Ioc v u))` as both
`u` and `v` tend to `l` so that `v ≤ u`.
See also `measure_integral_sub_linear_is_o_of_tendsto_ae_of_ge` for a version assuming
`[intervalIntegral.FTCFilter a l l']` and `[MeasureTheory.IsLocallyFiniteMeasure μ]`. If `l` is one
of `𝓝[≥] a`, `𝓝[≤] a`, `𝓝 a`, then it's easier to apply the non-primed version. The primed version
also works, e.g., for `l = l' = Filter.atTop`. -/
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge' [CompleteSpace E] [IsMeasurablyGenerated l']
[TendstoIxxClass Ioc l l'] (hfm : StronglyMeasurableAtFilter f l' μ) (hf : Tendsto f (l' ⊓ ae μ) (𝓝 c))
(hl : μ.FiniteAtFilter l') (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)) :=
(measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le' hfm hf hl hv hu huv).neg_left.congr_left fun t => by
simp [integral_symm (u t), add_comm]
