Kirszbraun theorem

TheoremKirszbraun extension theorem#✓fully proved

Let \(E\) be a real inner product space (not necessarily complete), let \(F\) be a complete real inner product space, let \(s \subseteq E\) and let \(K \ge 0\). Every map \(f : E \to F\) that is \(K\)-Lipschitz on \(s\) agrees on \(s\) with some map \(g : E \to F\) that is \(K\)-Lipschitz on all of \(E\).

theorem kirszbraun_general
    {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
    {s : Set E} {K : NNReal} {f : E → F}
    (hf : LipschitzOnWith K f s) :
    ∃ g : E → F, LipschitzWith K g ∧ Set.EqOn f g s

Sources

• M. Kirszbraun, Fund. Math. 22 (1934) 77-108 thesis; Valentine 1945 extension to Hilbert; Federer, Geometric Measure Theory, 2.10.43; the Lean theorem takes a real inner-product-space domain E and a complete real inner-product-space target F, with the same Lipschitz constant LipschitzWith K.

Used by 1

Used byKirszbraun extension theorem for Hilbert spaces

TheoremKirszbraun extension theorem for Hilbert spaces#✓fully proved

Let \(E\) and \(F\) be real Hilbert spaces, let \(s \subseteq E\) and let \(K \ge 0\). Every map \(f : E \to F\) that is \(K\)-Lipschitz on \(s\) agrees on \(s\) with some map \(g : E \to F\) that is \(K\)-Lipschitz on all of \(E\).

Completeness of \(E\) is not used: this is a special case of the Kirszbraun extension theorem for an arbitrary real inner product space domain.

@[nolint unusedArguments]
theorem kirszbraun
    {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
    {s : Set E} {K : NNReal} {f : E → F}
    (hf : LipschitzOnWith K f s) :
    ∃ g : E → F, LipschitzWith K g ∧ Set.EqOn f g s

Uses 1

Proof usesKirszbraun extension theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.