English
If f differentiable on a convex set with HasFDerivWithinAt bounds, then LipschitzOnWith on the set.
Русский
Если f дифференцируема на выпуклом множестве и имеет ограничение на производную внутри, тогда f Lipschitz на этом множестве.
LaTeX
$$$\text{If } hs: Convex\ Real\ s\text{ and } hder : HasFDerivWithinAt f (f' y) s y, \; bound... \Rightarrow LipschitzOnWith$$$
Lean4
/-- Let `s` be a convex set in a real normed vector space `E`, let `f : E → G` be a function
differentiable within `s` in a neighborhood of `x : E` with derivative `f'`. Suppose that `f'` is
continuous within `s` at `x`. Then for any number `K : ℝ≥0` larger than `‖f' x‖₊`, `f` is
`K`-Lipschitz on some neighborhood of `x` within `s`. See also
`Convex.exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt` for a version that claims
existence of `K` instead of an explicit estimate. -/
theorem exists_nhdsWithin_lipschitzOnWith_of_hasFDerivWithinAt_of_nnnorm_lt (hs : Convex ℝ s) {f : E → G}
(hder : ∀ᶠ y in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y) (hcont : ContinuousWithinAt f' s x) (K : ℝ≥0)
(hK : ‖f' x‖₊ < K) : ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t :=
by
obtain ⟨ε, ε0, hε⟩ : ∃ ε > 0, ball x ε ∩ s ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K} :=
mem_nhdsWithin_iff.1 (hder.and <| hcont.nnnorm.eventually (gt_mem_nhds hK))
rw [inter_comm] at hε
refine ⟨s ∩ ball x ε, inter_mem_nhdsWithin _ (ball_mem_nhds _ ε0), ?_⟩
exact
(hs.inter (convex_ball _ _)).lipschitzOnWith_of_nnnorm_hasFDerivWithin_le
(fun y hy => (hε hy).1.mono inter_subset_left) fun y hy => (hε hy).2.le
