Solution (source code)

= Solution

The necessary formulation uses a real <Hilbert space> $V$ of functions satisfying the essential <boundary conditions>, a continuous symmetric <bilinear form> $a$, and a continuous <linear functional> $\ell$. Assume constants $C,c>0$ with
$$
|a(v,w)|\leq C\|v\|_V\|w\|_V,\qquad
\boxed{a(v,v)\geq c\|v\|_V^2.}
$$
The latter is <coercivity>, the positive-definiteness condition needed in the chosen complete space. On the domain of the strong differential operator, <integration by parts> and the <boundary conditions> identify $a(v,w)=\langle\mathcal Lv,w\rangle$; this form extends to $V$. Let $\ell(w)=\langle f,w\rangle$ for admissible forcing. Define
$$
I(v)=a(v,v)-2\ell(v),\qquad
\boxed{u\text{ is a weak solution if }a(u,w)=\ell(w)\text{ for every }w\in V.}
$$
When $u$ has the regularity to belong to the strong operator domain, this is $\mathcal Lu=f$ with its <boundary conditions>. For complex spaces use a Hermitian form and $-2\operatorname{Re}\ell(v)$ to make the functional real.

Here is an existence proof by minimization. Continuity of $\ell$ and <coercivity> give $I(v)\geq c\|v\|_V^2-2\|\ell\|_{V^*}\|v\|_V$, so $m=\inf_VI$ is finite and a minimizing sequence $v_n$ is bounded. The quadratic parallelogram identity is
$$
I((v_n+v_j)/2)=\frac{I(v_n)+I(v_j)}2-\frac14a(v_n-v_j,v_n-v_j).
$$
Since its left side is at least $m$,
$$
a(v_n-v_j,v_n-v_j)\leq2\bigl(I(v_n)+I(v_j)-2m\bigr)\longrightarrow0.
$$
<Coercivity> makes $v_n$ Cauchy in $V$. <Completeness> gives $v_n\to u\in V$, and continuity of the form and forcing gives $I(u)=m$.

For every $w\in V$, differentiation along $u+tw$ yields
$$
0=\frac d{dt}I(u+tw)\bigg|_{t=0}=2a(u,w)-2\ell(w).
$$
Thus the <Euler-Lagrange equation> is exactly the stated <weak solution> equation. Conversely, if $u$ satisfies it, expansion gives
$$
\boxed{I(v)-I(u)=a(v-u,v-u)\geq c\|v-u\|_V^2.}
$$
This proves that the <weak solution> is the unique global minimum and that two <weak solutions> coincide. It proves the symmetric coercive case underlying the <Lax-Milgram theorem> directly, rather than taking existence as a theorem name. The framework is <symmetry and coercivity in quadratic energy minimization>.

The qualifications matter if positive definiteness is read more weakly. For a nonsymmetric operator the derivative of $\langle\mathcal Lv,v\rangle$ uses $(\mathcal L+\mathcal L^*)/2$, so it need not give $\mathcal Lu=f$. For example, on smooth periodic real functions $\mathcal L=1+\partial_x$ has $\langle\mathcal Lv,v\rangle=\|v\|_2^2$, but the functional's equation is $u=f$, not $u+u_x=f$. Even a symmetric operator can be strictly positive without being coercive: on <l2 sequence space>, $(Lv)_n=v_n/n$ with $f_n=1/n$ would require a solution $u_n=1$, which is not square summable. The associated functional has values $-\sum_{n=1}^N1/n$ on vectors with the first $N$ entries equal to one, so it has no minimum in that space. This is <strict positivity without coercivity can fail variational solvability>. Under the usual symmetric coercive meaning of positive definiteness, the proof above supplies every assertion requested.