English
If f is ContDiffOn on Icc(a,b), then the norm of f(b) − f(a) is bounded by the lintegral of the norm of its derivative over Icc(a,b).
Русский
Пусть f непрерывно дифференцируема на Icc(a,b); тогда ||f(b) − f(a)|| ≤ ∫_Icc(a,b) ||f'(x)|| dx.
LaTeX
$$$\\|f(b) - f(a)\\| \\\\le \\\\int_{a}^{b} \\|f'(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 ∂μ = ∫ 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 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' = 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' [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) :
(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 : ℝ) ∂μ :=
by
by_cases hE : CompleteSpace E; swap
· simp [intervalIntegral, integral, hE]
have A := hf.integral_sub_linear_isLittleO_ae hfm hl (hu.Ioc hv)
have B := hf.integral_sub_linear_isLittleO_ae hfm hl (hv.Ioc hu)
simp_rw [integral_const', sub_smul]
refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_
· cases le_total (u t) (v t) <;> simp [*]
· cases le_total (u t) (v t) <;> simp [*]
· simp_rw [intervalIntegral]
abel
