English
If f is ContDiffOn on Icc(a,b), then with derivWithin f on Icc, the same derivative bound holds: ||f(b) − f(a)|| ≤ ∫⁻_a^b ||derivWithin f (Icc a b) x|| dx.
Русский
Если f ∈ ContDiffOn на Icc(a,b), то неравенство аналогично предыдущему с derivWithin.
LaTeX
$$$\\|f(b) - f(a)\\| \\\\le \\\\int_{a}^{b} \\|\\operatorname{derivWithin} f (Icc(a,b)) (x)\\| \\, dx$$$
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 u v) • c + o(μ(Ioc u v))` as both
`u` and `v` tend to `l` so that `u ≤ v`.
See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le` 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_le' [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 : 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)) :=
(measure_integral_sub_linear_isLittleO_of_tendsto_ae' hfm hf hl hu hv).congr'
(huv.mono fun x hx => by simp [integral_const', hx]) (huv.mono fun x hx => by simp [integral_const', hx])
