README.md

This code was written as part of the 2023 MSRI "Formalization of Mathematics" workshop hosted in Berkeley California

Formal_Lipschitz

Implementation of Theorem 2.2 of "Metric Embeddings and Lipschitz Extentensions by Assaf Naor" page 5

Link: https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf

Code now integrated in Mathlib4 under :

Mathlib.Topology.MetricSpace.Kuratowski

Mathlib.Analysis.lpSpace

Mathlib.Topology.MetricSpace.Lipschitz

Theorem 2.2.

Suppose $(X,d_X)$ is a metric space, $A\subseteq X$ and let $f:A\to {\ell }_{\mathrm{\infty }}(\mathrm{\Gamma })$ a Lipschitz function. Then, there is an

extension $\tilde{f}:X\to {\ell }_{\mathrm{\infty }}(\mathrm{\Gamma })$ of $f$, i.e. with $\tilde{f}{|}_A=f$, such that $|\tilde{f}{|}_{\text{Lip }}=|f{|}_{\text{Lip }}$.

Proof.

Let $|f{|}_{\text{Lip }}=L$ and write

$$f(x)={(f_{\gamma }(x))}_{\gamma \in \mathrm{\Gamma }},\text{ for }x\in X\text{ and }{f}_{\gamma }(x)\in \mathbb{R}$$

Then, we see that

$$|f{|}_{\text{Lip }}=\underset{d_X(x,y)⩽1}{sup}\underset{\gamma \in \mathrm{\Gamma }}{sup}|f_{\gamma }(x)-f_{\gamma }(y)|=\underset{\gamma \in \mathrm{\Gamma }}{sup}{\left|f_{\gamma }\right|}_{\text{Lip }},$$

thus each $f_{\gamma }$ is also $L$-Lipschitz. Thus, it is enough to extend all the $f_{\gamma }$ isometrically, that is prove our theorem with $\mathbb{R}$ replacing ${\ell }_{\mathrm{\infty }}(\mathrm{\Gamma })$. This will be done in the next important lemma.

Lemma 2.3

(Nonlinear Hahn-Banach theorem). Suppose $(X,d_X)$ is a metric space, $A\subseteq X$ and let $f:A\to \mathbb{R}$ a Lipschitz function.

Then, there is an extension $\tilde{f}:X\to \mathbb{R}$ of $f$, i.e. with ${\tilde{f}|}_A=f$, such that $|\tilde{f}{|}_{\text{Lip }}=|f{|}_{\text{Lip }}$

First-direct proof. Call again $L=|f{|}_{\text{Lip }}$ and define the function $\tilde{f}:X\to \mathbb{R}$ by the formula

$$\tilde{f}(x)=\underset{a\in A}{inf}\{f(a)+L{d}_X(x,a)\},x\in X$$

To see that this function satisfies the results, fix an arbitrary $a_0\in A$. Then, for any $a\in A$ :

$$f(a)+L{d}_X(x,a)⩾f\left(a_0\right)-Ld(a,a_0)+Ld(x,a)⩾f\left(a_0\right)-Ld(x,a_0)>-\mathrm{\infty },$$

so $\tilde{f}(x)$ is well-defined. Also, if $x\in A$, the above shows that $\tilde{f}(x)=f(x)$. Finally, for $x,y\in X$ and $\epsilon >0$, choose $a_x\in A$ such that

$$\tilde{f}(x)⩾f\left(a_x\right)+Ld(x,a_x)-\epsilon$$

Then,

$$\tilde{f}(y)-\tilde{f}(x)⩽f\left(a_x\right)+Ld(y,a_x)-f\left(a_x\right)-Ld(x,a_x)+\epsilon ⩽Ld(x,y)+\epsilon .$$

Thus, we see that $\tilde{f}$ is indeed $L$-Lipschitz.