English
For a finite index set ι, a function f: α → ι → ℝ that is K-Lipschitz on s has a K-Lipschitz extension g: α → ι → ℝ with f and g agreeing on s.
Русский
Для конечного множества индексов ι функция f: α → ι → ℝ, локально липшицева с константой K на s, имеет продолжение g: α → ι → ℝ, сохраняющее локальную липшицкость и совпадающее с f на s.
LaTeX
$$$[\\text{Fintype } \\iota] \\; (\\text{LipschitzOnWith } K\to f\\,s) \\Rightarrow \\exists g:\\alpha\\to\\iota\\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. The same result for the space `ℓ^∞ (ι, ℝ)` over a possibly infinite
type `ι` is implemented in `LipschitzOnWith.extend_lp_infty`. -/
theorem extend_pi [Fintype ι] {f : α → ι → ℝ} {s : Set α} {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s :=
by
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i =>
by
have : LipschitzOnWith K (fun x : α => f x i) s :=
LipschitzOnWith.of_dist_le_mul fun x hx y hy => (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
exact this.extend_real
choose g hg using this
refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩
· exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y
· ext1 i
exact (hg i).2 hx
