Prolongement d'une forme linéaire continue

Encore un énoncé faux ( unicité?)

Si ton s.e.v n'est pas dense c'est mal barré.

Il faut commencer par montrer que pour tout $f\in F'$ l'extension existe :

Soit $(e_n)$ une famille de $F$ qui est une base orthonormale de $\overline{F}$, si $\sum_n |f(e_n)|^2 <\infty$ alors $$v = \sum_n \overline{f(e_n)} e_n \in \overline{F}, \qquad \forall x\in F, f(x)=\langle x,v\rangle$$ (regarder $g(x)=f(x)-\langle x,v\rangle$, c'est une forme linéaire continue sur $F$ et elle est nulle sur le sous-espace $Vect((e_n))$ qui est dense)
et $\langle.,v\rangle $ est aussi une forme linéaire $\in\overline{F}'$ et $\in H'$.

Sinon $\sum_n |f(e_n)|^2 = \infty$ et on peut construire une suite $y_k = c_k \sum_{n=1}^k \overline{f(e_n)} e_n \in F$ telle que $y_k \to 0 $ et $f(y_k) \to \infty$ ce qui contredit que $f\in F'$.

Avec le même argument de base orthonormale appliqué à $H$ on a que toute extension de $f$ à $H$ sera de la forme $f(x)=\langle x,w\rangle$ pour un $w\in H$.
Et $$\forall x\in F, \langle x,w-v\rangle=0 \iff \quad w-v\in F^\perp$$
Donc l'extension de $F'$ à $H'$ se fait en choisissant un $w-v\in F^\perp$, comme on veut.

J'ai donné une approche totalement élémentaire, en gros Hahn-Banach c'est le truc abstrait qu'on utilise dans les espaces plus compliqués, pas dans les Hilbert.

supp

@Riemann_lapins_cretins
Ce que tu développes c'est Hahn-Banach forme analytique et en bonus, appliquée dans un Hilbert donne l'unicité du prolongement (l unicité vient du fait qu'un Hilbert est strictement convexe)

Je te vois tourner en rond. Est-ce que j'ai dit que l'existence pose probleme. Relis mon premier message. Sans hypothèses supplémentaires, tu n'as pas l'unicité.