English
Given a K-Lipschitz map on a subset, there exists an extension to the whole space with constant LipschitzExtensionConstant(E')·K.
Русский
Пусть имеется отображение, удовлетворяющее условию Lip, на подмножестве; существует его продолжение на всё пространство с константой LipschitzExtensionConstant(E')·K.
LaTeX
$${hf : LipschitzOnWith K f s} ⇒ ∃ g, LipschitzWith (lipschitzExtensionConstant(E')·K) g ∧ EqOn f g s$$
Lean4
/-- Any `K`-Lipschitz map from a subset `s` of a metric space `α` to a finite-dimensional real
vector space `E'` can be extended to a Lipschitz map on the whole space `α`, with a slightly worse
constant `lipschitzExtensionConstant E' * K`. -/
theorem extend_finite_dimension {α : Type*} [PseudoMetricSpace α] {E' : Type*} [NormedAddCommGroup E']
[NormedSpace ℝ E'] [FiniteDimensional ℝ E'] {s : Set α} {f : α → E'} {K : ℝ≥0} (hf : LipschitzOnWith K f s) :
∃ g : α → E', LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s := by
/- This result is already known for spaces `ι → ℝ`. We use a continuous linear equiv between
`E'` and such a space to transfer the result to `E'`. -/
let ι : Type _ := Basis.ofVectorSpaceIndex ℝ E'
let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz
have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s := LA.comp_lipschitzOnWith hf
obtain ⟨g, hg, gs⟩ : ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=
L.extend_pi
refine ⟨A.symm ∘ g, ?_, ?_⟩
· have LAsymm : LipschitzWith ‖A.symm.toContinuousLinearMap‖₊ A.symm := by apply A.symm.lipschitz
apply (LAsymm.comp hg).weaken
rw [lipschitzExtensionConstant, ← mul_assoc]
exact mul_le_mul' (le_max_left _ _) le_rfl
· intro x hx
have : A (f x) = g x := gs hx
simp only [(· ∘ ·), ← this, A.symm_apply_apply]
