English
If f is C^1 on the closed interval Icc(a,b) with a ≤ b, then the difference f(b) − f(a) is controlled by the integral of the norm of f' over [a,b]: ||f(b) − f(a)|| ≤ ∫_a^b ||f'(x)|| dx.
Русский
Пусть f: ℝ → E является C^1 на отрезке Icc(a,b) и a ≤ b. Тогда ||f(b) − f(a)|| ≤ ∫_a^b ||f'(x)|| dx.
LaTeX
$$$\\|f(b) - f(a)\\| \\\\le \\\\int_{a}^{b} \\|f'(x)\\| \\, dx$$$
Lean4
theorem enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc (h : ContDiffOn ℝ 1 f (Icc a b)) (hab : a ≤ b) :
‖f b - f a‖ₑ ≤ ∫⁻ x in Icc a b, ‖deriv f x‖ₑ := by
/- We want to write `f b - f a = ∫ x in Icc a b, deriv f x` and use the inequality between
norm of integral and integral of norm. There is a small difficulty that this formula is not
true when `E` is not complete, so we need to go first to the completion, and argue there. -/
let g := UniformSpace.Completion.toComplₗᵢ (𝕜 := ℝ) (E := E)
have : ‖(g ∘ f) b - (g ∘ f) a‖ₑ = ‖f b - f a‖ₑ := by
rw [← edist_eq_enorm_sub, Function.comp_def, g.isometry.edist_eq, edist_eq_enorm_sub]
rw [← this, ← integral_deriv_of_contDiffOn_Icc (g.contDiff.comp_contDiffOn h) hab, integral_of_le hab,
restrict_Ioc_eq_restrict_Icc]
apply (enorm_integral_le_lintegral_enorm _).trans
apply lintegral_mono_ae
rw [← restrict_Ioo_eq_restrict_Icc]
filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
rw [fderiv_comp_deriv]; rotate_left
· exact (g.contDiff.differentiable le_rfl).differentiableAt
· exact ((h x ⟨hx.1.le, hx.2.le⟩).contDiffAt (Icc_mem_nhds hx.1 hx.2)).differentiableAt le_rfl
have : fderiv ℝ g (f x) = g.toContinuousLinearMap := g.toContinuousLinearMap.fderiv
simp [this]
