English
For a locally finite measure μ and FTCFilter a l l', the quantity ∫ x in u t..v t f x ∂μ minus ∫ x in u t..v t c ∂μ is little-o of ∫ x in u t..v t 1 ∂μ as t → lt, under suitable measurability/limit hypotheses.
Русский
Для локально ограниченной меры μ и FTCFilter a l l' верно, что разность интегралов является little-o от интеграла единицы при стремлении t к l.
LaTeX
$$$(∫_{u(t)}^{v(t)} f(x) \\, dμ) - (∫_{u(t)}^{v(t)} c \\, dμ) = o\\,[lt](∫_{u(t)}^{v(t)} 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 ∂μ = ∫ x in u..v, c ∂μ + o(∫ x in u..v, 1 ∂μ)` as both `u` and `v` tend to `l`.
See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae'` for a version that also works, e.g.,
for `l = l' = Filter.atTop`.
We use integrals of constants instead of measures because this way it is easier to formulate
a statement that works in both cases `u ≤ v` and `v ≤ u`. -/
theorem measure_integral_sub_linear_isLittleO_of_tendsto_ae [FTCFilter a l l'] (hfm : StronglyMeasurableAtFilter f l' μ)
(hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)) (hu : Tendsto u lt l) (hv : Tendsto v lt l) :
(fun t => (∫ x in u t..v t, f x ∂μ) - ∫ _ in u t..v t, c ∂μ) =o[lt] fun t => ∫ _ in u t..v t, (1 : ℝ) ∂μ :=
haveI := FTCFilter.meas_gen l
measure_integral_sub_linear_isLittleO_of_tendsto_ae' hfm hf (FTCFilter.finiteAt_inner l) hu hv
