Démonstration. D’une part, $$\Vert x+y{\Vert }^2=⟨x+y,x+y⟩=\Vert x{\Vert }^2+\Vert y{\Vert }^2+2⟨x,y⟩$$ D’autre part, $$\Vert x-y{\Vert }^2=⟨x-y,x-y⟩=\Vert x{\Vert }^2+\Vert y{\Vert }^2-2⟨x,y⟩$$ En additionnant les deux lignes, on obtient bien l’égalité voulue. ◻

Démonstration. Soit $x\in H$. Posons $\delta =d(x,C)$. Par la caractérisation séquentielle de la borne inférieure, il existe $(y_n)$ une suite de $C$ telle que $\Vert x-y_n\Vert ⟶\delta$. Montrons que $(y_n)$ est une suite de Cauchy. On applique le Lemme 1 : $$\forall p,q\in \mathbb{N},\Vert (x-y_p)+(x-y_q){\Vert }^2+\Vert y_p-y_q{\Vert }^2=2(\Vert x-y_p{\Vert }^2+\Vert x-y_q{\Vert }^2)\text{\hspace{1em}(∗∗)}$$ Or, $C$ est convexe. Donc $\forall p,q\in \mathbb{N}$, $\frac{y_p+y_q}{2}\in C$. Par définition, $$\begin{array}{rl}& \Vert x-\frac{y_p+y_q}{2}\Vert \ge \delta \\ ⟺& \frac{1}{2}\Vert (x-y_p)+(x-y_q)\Vert \ge \delta \\ ⟺& \Vert (x-y_p)+(x-y_q){\Vert }^2\ge 4{\delta }^2\end{array}$$ Par $(\ast \ast )$, quand $p,q⟶+\infty$ : $$\Vert y_p-y_q\Vert \le 2((\underset{⟶{\delta }^2}{\underbrace{\Vert x-y_p{\Vert }^2}}-{\delta }^2)+(\underset{⟶{\delta }^2}{\underbrace{\Vert x-y_q{\Vert }^2}}-{\delta }^2))⟶0$$ Ainsi $(y_n)$ est une suite de Cauchy de $H$ qui est complet, donc $(y_n)$ converge vers $y\in H$. Mais, $C$ est fermé et $(y_n)$ est une suite de $C$, donc $y\in C$.

Montrons maintenant que $y$ est unique. Soit $z\in C$ tel que $\delta =\Vert x-z\Vert$. On définit la suite $(z_n)$ par $$\forall n\in \mathbb{N},z_n=\{\begin{array}{ll}y& \text{si }n\text{ est pair}\\ z& \text{si }n\text{ est impair}\end{array}$$ Cette suite vérifie $\forall n\in \mathbb{N}$, $\Vert x-z_n\Vert =\delta$ donc en particulier $\Vert x-z_n\Vert ⟶\delta$, et on peut tout-à-fait refaire le raisonnement précédent pour montrer que $(z_n)$ converge (vers $y=z$, donc). Ainsi, on a bien existence et unicité du projeté.

Soit $y\in C$ vérifiant $(\ast )$. Montrons que $y=P_C(x)$. $\forall z\in C$, $$\begin{array}{rl}\Vert z-x{\Vert }^2& =\Vert (z-y)-(x-y){\Vert }^2\\ & =\Vert z-y{\Vert }^2+\Vert x-y{\Vert }^2-2⟨z-y,x-y⟩\\ & \ge \Vert z-y{\Vert }^2+\Vert x-y{\Vert }^2\\ & \ge \Vert x-y{\Vert }^2\end{array}$$ ie. $\Vert z-x\Vert \ge \Vert x-y\Vert$. De plus, $y\in C$, donc $d(y,C)=d(x,C)$. D’où $y=P_C(x)$.

Montrons maintenant que $P_C(x)$ vérifie bien $(\ast )$. $\forall z\in C$, on a $$\Vert x-z{\Vert }^2\ge \Vert x-P_C(x){\Vert }^2$$ Or, en développant : $$\begin{array}{rl}\Vert x-z{\Vert }^2& =\Vert (x-P_C(x))-(z-P_C(x)){\Vert }^2\\ & =\Vert x-P_C(x){\Vert }^2+\Vert z-P_C(x){\Vert }^2-2⟨x-P_C(x),z-P_C(x)⟩\\ & \ge \Vert x-P_C(x){\Vert }^2\end{array}$$ D’où, par la dernière inégalité, $$\Vert z-P_C(x){\Vert }^2-2⟨x-P_C(x),z-P_C(x)⟩\ge 0\text{\hspace{1em}(∗∗∗)}$$ Soit maintenant $z_0\in C$. On va appliquer $(\ast \ast \ast )$ à $z=\lambda z_0+(1-\lambda )z_0\in C$ pour $\lambda \in ]0,1]$ : $$\begin{array}{rl}& {\lambda }^2\Vert z_0+P_C(x){\Vert }^2-2\lambda ⟨x-P_C(x),z_0-P_C(x)⟩\ge 0\\ ⟹& \lambda \Vert z_0+P_C(x){\Vert }^2-2⟨x-P_C(x),z_0-P_C(x)⟩\ge 0\\ \stackrel{\lambda ⟶0}{⟹}& -2⟨x-P_C(x),z_0-P_C(x)⟩\ge 0\end{array}$$ ce que l’on voulait. ◻

Démonstration. Si $x\in F\cap F^{\perp }$, alors $\Vert x\Vert =⟨x,x⟩=0$, et donc $x=0$. Montrons maintenant que $F+F^{\perp }=H$. Soit $x\in H$. Comme $F$ est un convexe fermé de $H$ (en tant que sous-espace vectoriel fermé), on peut appliquer le Théorème 3. Ainsi, il existe un unique $P_F(x)\in F$ tel que $d(x,F)=d(x,P_F(x))$ et $$\forall z\in F,⟨x-P_F(x),z-P_F(x)⟩\le 0\text{\hspace{1em}(∗)}$$ Soit $z_0\in F$. on peut appliquer $(\ast )$ à $z=z_0$ : $$⟨x-P_F(x),z_0-P_F(x)⟩\le 0$$ On va également appliquer $(\ast )$ à $z=-z_0+2P_F(x)\in F$ : $$⟨x-P_F(x),-z_0+P_F(x)⟩\le 0⟺⟨x-P_F(x),z_0-P_F(x)⟩\ge 0$$ Ce qui montre que l’inégalité de $(\ast )$ est en fait une égalité. On en tire : $$\forall z\in F,⟨x-P_F(x),z⟩=⟨x-P_F(x),z-P_F(x)⟩-⟨x-P_F(x),0-P_F(x)⟩=0$$ donc $x-P_F(x)\in F^{\perp }$. En conclusion, on a : $$x=\underset{\in F}{\underbrace{P_F(x)}}+\underset{\in F^{\perp }}{\underbrace{x-P_F(x)}}\in F+F^{\perp }$$ et on a donc bien la somme directe $H=F\oplus F^{\perp }$. ◻