English
If there is a fixed linear map φ and a bound C on how far the derivative f' can deviate from φ on s, then f(y)−f(x)−φ(y−x) is bounded by C ‖y−x‖ for x,y∈s.
Русский
Если на s существует фиксированная линейная карта φ и существует предел отклонения производной f' от φ в пределах s равный C, то разность f(y)−f(x)−φ(y−x) ограничена величиной C ‖y−x‖ при x,y∈s.
LaTeX
$$$\forall x,y\in s:\ ||f(y)-f(x)-\phi(y-x)|| \le C\,||y-x||,$ где $f'$ удовлетворяет HasFDerivWithinAt и $\|f'(x)-\phi\|≤C$ для всех $x\in s$.$$
Lean4
/-- Variant of the mean value inequality on a convex set, using a bound on the difference between
the derivative and a fixed linear map, rather than a bound on the derivative itself. Version with
`HasFDerivWithinAt`. -/
theorem norm_image_sub_le_of_norm_hasFDerivWithin_le' (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
(bound : ∀ x ∈ s, ‖f' x - φ‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖ := by
/- We subtract `φ` to define a new function `g` for which `g' = 0`, for which the previous theorem
applies, `Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le`. Then, we just need to glue
together the pieces, expressing back `f` in terms of `g`. -/
let g y := f y - φ y
have hg : ∀ x ∈ s, HasFDerivWithinAt g (f' x - φ) s x := fun x xs => (hf x xs).sub φ.hasFDerivWithinAt
calc
‖f y - f x - φ (y - x)‖ = ‖f y - f x - (φ y - φ x)‖ := by simp
_ = ‖f y - φ y - (f x - φ x)‖ := by congr 1; abel
_ = ‖g y - g x‖ := by simp [g]
_ ≤ C * ‖y - x‖ := Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le hg bound hs xs ys
