English
If a function f: α → ℓ^∞(ι) is K-Lipschitz on a subset s, there exists an extension g: α → ℓ^∞(ι) with the same Lipschitz constant and f = g on s.
Русский
Если функция f: α → ℓ^∞(ι) сла Lipshitz на подмножестве s, существует продолжение g: α → ℓ^∞(ι) той же константы Липшица и такое, что f = g на s.
LaTeX
$$$\exists g: α \to ℓ^∞(ι),\ LipschitzWith K g \land 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 2.2 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015]
The same result for the case of a finite type `ι` is implemented in
`LipschitzOnWith.extend_pi`.
-/
theorem extend_lp_infty [PseudoMetricSpace α] {s : Set α} {ι : Type*} {f : α → ℓ^∞(ι)} {K : ℝ≥0}
(hfl : LipschitzOnWith K f s) : ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
-- Construct the coordinate-wise extensions
rw [LipschitzOnWith.coordinate] at hfl
have (i : ι) : ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s :=
LipschitzOnWith.extend_real
(hfl i) -- use the nonlinear Hahn-Banach theorem here!
choose g hgl hgeq using this
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
· exact ⟨0, LipschitzWith.const' 0, by simp⟩
· -- Show that the extensions are uniformly bounded
have hf_extb : ∀ a : α, Memℓp (swap g a) ∞ :=
by
apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
use ‖f a₀‖
rintro - ⟨i, rfl⟩
simp_rw [← hgeq i ha₀_in_s]
exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
let f_ext' : α → ℓ^∞(ι) := fun i ↦ ⟨swap g i, hf_extb i⟩
refine ⟨f_ext', ?_, ?_⟩
· rw [LipschitzWith.coordinate]
exact hgl
· intro a hyp
ext i
exact (hgeq i) hyp
