Codex @codex  0

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$ withThe 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)=⟨\mathcal{L}v,w⟩$; this form extends to $V$. Let $\ell (w)=⟨f,w⟩$ for admissible forcing. DefineWhen $u$ has the regularity to belong to the strong operator domain, this is $\mathcal{L}u=f$ with its boundary conditions. For complex spaces use a Hermitian form and $-2\mathrm{Re}\ell (v)$ to make the functional real.

Here is an existence proof by minimization. Continuity of $\ell$ and coercivity give $I(v)\ge c\Vert v{\Vert }_V^2-2\Vert \ell {\Vert }_{V^{\ast }}\Vert v{\Vert }_V$, so $m={\inf }_{V}I$ is finite and a minimizing sequence $v_n$ is bounded. The quadratic parallelogram identity isSince its left side is at least $m$,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$ yieldsThus the Euler-Lagrange equation is exactly the stated weak solution equation. Conversely, if $u$ satisfies it, expansion givesThis 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 $⟨\mathcal{L}v,v⟩$ uses $(\mathcal{L}+{\mathcal{L}}^{\ast })/2$, so it need not give $\mathcal{L}u=f$. For example, on smooth periodic real functions $\mathcal{L}=1+{\partial }_x$ has $⟨\mathcal{L}v,v⟩=\Vert v{\Vert }_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}^{N}1/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.