English
A function f: α → ℝ that is K-Lipschitz on a subset s admits a K-Lipschitz extension g to the whole space, with g equal to f on s.
Русский
Функция f: α → ℝ, локально липшицева с константой K на подмножестве s, допускает продолжение g на всю пространственность с той же константой, причём g совпадает с f на s.
LaTeX
$$$\\exists g: \\alpha \\to \\mathbb{R}, \\ \\text{LipschitzWith}(K, g) \\land \\operatorname{EqOn}(f, g, s).$$$
Lean4
/-- A function `f : α → ℝ` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz extension
to the whole space. -/
theorem extend_real {f : α → ℝ} {s : Set α} {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
∃ g : α → ℝ, LipschitzWith K g ∧ EqOn f g s := by
/- An extension is given by `g y = Inf {f x + K * dist y x | x ∈ s}`. Taking `x = y`, one has
`g y ≤ f y` for `y ∈ s`, and the other inequality holds because `f` is `K`-Lipschitz, so that it
cannot counterbalance the growth of `K * dist y x`. One readily checks from the formula that
the extended function is also `K`-Lipschitz. -/
rcases eq_empty_or_nonempty s with (rfl | hs)
· exact ⟨fun _ => 0, (LipschitzWith.const _).weaken (zero_le _), eqOn_empty _ _⟩
have : Nonempty s := by simp only [hs, nonempty_coe_sort]
let g := fun y : α => iInf fun x : s => f x + K * dist y x
have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y =>
by
rcases hs with ⟨z, hz⟩
refine ⟨f z - K * dist y z, ?_⟩
rintro w ⟨t, rfl⟩
dsimp
rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
calc
f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
_ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
have E : EqOn f g s := fun x hx =>
by
refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_
simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩
rw [← sub_le_iff_le_add]
refine le_ciInf fun z => ?_
rw [sub_le_iff_le_add]
calc
g x ≤ f z + K * dist x z := ciInf_le (B x) _
_ ≤ f z + K * dist y z + K * dist x y :=
by
rw [add_assoc, ← mul_add, add_comm (dist y z)]
gcongr
apply dist_triangle
