English
If f is C^1 within a convex set s at x, then f is Lipschitz on a neighborhood of x within s.
Русский
Если функция C^1 внутри выпуклого множества s в точке x, то она Lipschitz на окрестности x внутри s.
LaTeX
$$$ContDiffWithinAt\\ 𝕂\\ 1 f s x \\Rightarrow ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t$$$
Lean4
/-- If `f` is `C^1` within a convex set `s` at `x`, then it is Lipschitz on a neighborhood of `x`
within `s`. -/
theorem exists_lipschitzOnWith {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
[NormedSpace ℝ F] {f : E → F} {s : Set E} {x : E} (hf : ContDiffWithinAt ℝ 1 f s x) (hs : Convex ℝ s) :
∃ K : ℝ≥0, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t :=
by
rcases hf 1 le_rfl with ⟨t, hst, p, hp⟩
rcases Metric.mem_nhdsWithin_iff.mp hst with ⟨ε, ε0, hε⟩
replace hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s) := hp.mono hε
clear hst hε t
rw [← insert_eq_of_mem (Metric.mem_ball_self ε0), ← insert_inter_distrib] at hp
rcases hp.exists_lipschitzOnWith ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩
rw [inter_comm, ← nhdsWithin_restrict' _ (Metric.ball_mem_nhds _ ε0)] at hst
exact ⟨K, t, hst, hft⟩
