English
If f is convex on a ball B(x0,r), r' < r and the image f(B(x0,r)) is bounded, then f is Lipschitz on B(x0,r') with some finite constant K.
Русский
Если f выпукла на шаре B(x0,r), при этом r' < r и образ f(B(x0,r)) ограничен, то f является липшицевой на B(x0,r') с некоторой конечной константой K.
LaTeX
$$$\\exists K,\\; \\text{LipschitzOnWith}(K,\n f,\n B(x_0,r'))$$$
Lean4
theorem lipschitzOnWith_of_abs_le (hf : ConvexOn ℝ (ball x₀ r) f) (hε : 0 < ε) (hM : ∀ a, dist a x₀ < r → |f a| ≤ M) :
LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε)) :=
by
set K := 2 * M / ε with hK
have oneside {x y : E} (hx : x ∈ ball x₀ (r - ε)) (hy : y ∈ ball x₀ (r - ε)) : f x - f y ≤ K * ‖x - y‖ :=
by
obtain rfl | hxy := eq_or_ne x y
· simp
have hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r := ball_subset_ball <| by linarith
have hx' : x ∈ ball x₀ r := hx₀r hx
have hy' : y ∈ ball x₀ r := hx₀r hy
let z := x + (ε / ‖x - y‖) • (x - y)
replace hxy : 0 < ‖x - y‖ := by rwa [norm_sub_pos_iff]
have hz : z ∈ ball x₀ r :=
mem_ball_iff_norm.2 <| by
calc
_ = ‖(x - x₀) + (ε / ‖x - y‖) • (x - y)‖ := by simp only [z, add_sub_right_comm]
_ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖ := norm_add_le ..
_ < r - ε + ε :=
(add_lt_add_of_lt_of_le (mem_ball_iff_norm.1 hx) <| by simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne'])
_ = r := by simp
let a := ε / (ε + ‖x - y‖)
let b := ‖x - y‖ / (ε + ‖x - y‖)
have hab : a + b = 1 := by simp [field, a, b]
have hxyz : x = a • y + b • z := by
calc
x = a • x + b • x := by rw [Convex.combo_self hab]
_ = a • y + b • z := by simp [z, a, b, smul_smul, hxy.ne', smul_sub]; abel
rw [hK, mul_comm, ← mul_div_assoc, le_div_iff₀' hε]
calc
ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x) :=
by
have h := hf.2 hy' hz (by positivity) (by positivity) hab
simp only [← hxyz, smul_eq_mul, a, b] at h
field_simp at h
linear_combination h
_ ≤ _ := by
rw [sub_eq_add_neg (f _), two_mul]
gcongr
· exact (le_abs_self _).trans <| hM _ hz
· exact (neg_le_abs _).trans <| hM _ hx'
refine .of_dist_le' fun x hx y hy ↦ ?_
simp_rw [dist_eq_norm_sub, Real.norm_eq_abs, abs_sub_le_iff]
exact ⟨oneside hx hy, norm_sub_rev x _ ▸ oneside hy hx⟩
