approximatesLinearOn_iff_lipschitzOnWith

English

ApproximatesLinearOn is equivalent to LipschitzOnWith for the difference f−f' on a set s.

Русский

Неявная линейность эквивалентна условиям Липшица для разности f−f' на множестве s.

LaTeX

$$$ ApproximatesLinearOn\ f\ f'\ s\ c \;\Leftrightarrow\; LipschitzOnWith\ c\ (f - \!\!\!\!\!\!\! \!\!\!f')\ s$$$

Lean4

theorem approximatesLinearOn_iff_lipschitzOnWith {f : E → F} {f' : E →L[𝕜] F} {s : Set E} {c : ℝ≥0} :
    ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s :=
  by
  have : ∀ x y, f x - f y - f' (x - y) = (f - f') x - (f - f') y := fun x y ↦ by simp only [map_sub, Pi.sub_apply]; abel
  simp only [this, lipschitzOnWith_iff_norm_sub_le, ApproximatesLinearOn]

Похожие утверждения