CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Symmetric Lax--Milgram is energy minimisation

Statement

Assume Countable Choice. Let $a$ be a bounded coercive symmetric sesquilinear form on a real or complex Hilbert space $H$ with coercivity constant $α > 0$ and let $F$ be a bounded conjugate-linear functional, with $u$ the Lax--Milgram solution of The Lax--Milgram theorem. Then the functional $J (v) : = \frac{1}{2} Re a (v, v) - Re F (v)$ is real valued and attains its strict minimum on $H$ at $u$ : $J (v) > J (u)$ for every $v \neq u$ . In the real case $J (v) = \frac{1}{2} a (v, v) - F (v)$ , and in the complex case $a (v, v)$ is already real by symmetry, so $J (v) = \frac{1}{2} a (v, v) - Re F (v)$ ; no claim is made that a nonsymmetric form has such a minimisation. Consequently the solution is characterised by the minimisation problem independently of uniqueness in The Lax--Milgram theorem.

Facts & Assumptions

Given: Countable Choice; a real or complex Hilbert space $H$ ; a bounded coercive symmetric sesquilinear form $a$ with coercivity constant $α > 0$ ; a bounded conjugate-linear functional $F$ ; the Lax--Milgram solution $u$ with $a (u, v) = F (v)$ for all $v$ ; and $J (v) = \frac{1}{2} Re a (v, v) - Re F (v)$ .

[F1]

Symmetry makes $a (v, v)$ real: $a (v, v) = \overline{a (v, v)}$ , so $Re a (v, v) = a (v, v)$ ; coercivity gives $Re a (w, w) \geq α ∥ w ∥^{2}$ ; and $a$ is linear in the first argument and conjugate-linear in the second, so $a$ is additive in each slot and $a (w, u) = \overline{a (u, w)}$ by symmetry (Bounded, coercive and symmetric sesquilinear forms, The induced length is a norm).

[F2]

The solution satisfies $a (u, w) = F (w)$ for every $w \in H$ ; existence and uniqueness are those of Lax--Milgram (The Lax--Milgram theorem).

[F3]

Real parts: $Re z + Re \overline{z} = 2 Re z$ and $Re (z_{1} + z_{2}) = Re z_{1} + Re z_{2}$ (Real and imaginary parts, complex conjugation, and modulus, Hilbert space).

Proof

1.1F1F3algebra

Expansion: write $v = u + w$ with $w : = v - u$ . Using additivity in both slots, symmetry and [F3], $Re a (v, v) = Re a (u, u) + Re (a (u, w) + \overline{a (u, w)}) + Re a (w, w) = Re a (u, u) + 2 Re a (u, w) + Re a (w, w),$ while $Re F (v) = Re F (u) + Re F (w)$ , so $J (v) - J (u) = \frac{1}{2} Re a (w, w) + Re a (u, w) - Re F (w) .$

2.1F1F2step 1.1

The linear term vanishes: by [F2], $a (u, w) = F (w)$ , hence $Re a (u, w) - Re F (w) = 0$ , and $J (v) - J (u) = \frac{1}{2} Re a (w, w) \geq \frac{α}{2} ∥ w ∥^{2}$ by coercivity.

3.1F1F3step 2.1∎

Strict minimum: the right-hand side is positive whenever $w \neq 0$ ; hence $J (v) > J (u)$ for every $v \neq u$ , so $J$ is real valued and attains its strict minimum at the Lax--Milgram solution $u$ . In the real case $Re$ is the identity and $J (v) = \frac{1}{2} a (v, v) - F (v)$ ; in the complex case symmetry makes $a (v, v)$ real, so taking its real part is redundant, while $Re F (v)$ ensures a real-valued functional. No minimisation claim is made for nonsymmetric forms.

Depends on

Used by

A coercive form need not be symmetric Counterexample
A nonsymmetric coercive elliptic form Example
Nonsymmetric Lax--Milgram is not a scalar minimisation principle Remark

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)