English
Let hf be a convex function on a ball. If the image f(B(x0,r)) is bounded, then there exists K such that f is Lipschitz on a smaller ball B(x0,r').
Русский
Пусть hf выпукла на шаре; если образ f(B(x0,r)) ограничен, то существует константа K, такая что f Lip-ограничена на меньшем шаре B(x0,r').
LaTeX
$$$\\exists K,\\; \\text{LipschitzOnWith}(K)\\ f\\ (\\mathrm{ball}\\ x_0,r')$$$
Lean4
theorem exists_lipschitzOnWith_of_isBounded (hf : ConvexOn ℝ (ball x₀ r) f) (hr : r' < r)
(hf' : IsBounded (f '' ball x₀ r)) : ∃ K, LipschitzOnWith K f (ball x₀ r') :=
by
rw [isBounded_iff_subset_ball 0] at hf'
simp only [Set.subset_def, mem_image, mem_ball, dist_zero_right, Real.norm_eq_abs, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂] at hf'
obtain ⟨M, hM⟩ := hf'
rw [← sub_sub_cancel r r']
exact ⟨_, hf.lipschitzOnWith_of_abs_le (sub_pos.2 hr) fun a ha ↦ (hM a ha).le⟩
