CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The Lax--Milgram solution operator has norm at most $1 / α$

Statement

Under the hypotheses of The Lax--Milgram theorem, let $F$ be the space of bounded conjugate-linear functionals on $H$ , normed by $∥ F ∥ = \sup_{∥ v ∥ \leq 1} ∣ F (v) ∣$ , and let $S : F \to H$ assign to $F$ the unique solution $u$ of $a (u, v) = F (v)$ for all $v$ . Then $S$ is well defined and linear, and $∥ S ∥ \leq \frac{1}{α} .$ In particular $∥ u ∥ \leq ∥ F ∥ / α$ for every $F$ , and the estimate is uniform over all data.

Facts & Assumptions

Given: Countable Choice; a real or complex Hilbert space $H$ ; a bounded coercive sesquilinear form $a$ with constants $M, α$ ; the normed space $F$ of bounded conjugate-linear functionals on $H$ with $∥ F ∥ = \sup_{∥ v ∥ \leq 1} ∣ F (v) ∣$ ; and the solution map $S : F \to H$ sending $F$ to the unique $u$ with $a (u, v) = F (v)$ for all $v$ .

[F1]

Lax--Milgram: for every $F \in F$ there is exactly one $u \in H$ with $a (u, v) = F (v)$ for all $v$ , and $α ∥ u ∥ \leq ∥ F ∥$ ; the form is linear in the first argument (The Lax--Milgram theorem, Bounded, coercive and symmetric sesquilinear forms, Hilbert space).

[F2]

Bounded operators and operator norm: $∥ S ∥ = \sup {∥ S F ∥ : ∥ F ∥ \leq 1}$ , and $S$ is bounded with $∥ S ∥ \leq 1 / α$ once $∥ S F ∥ \leq ∥ F ∥ / α$ for every $F$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum, A bounded linear operator between normed spaces, The spaces (\mathcal B(X,Y)) and (\mathcal B(X)) of bounded linear operators).

Proof

1.1F1

$S$ is well defined by [F1]: each $F$ has exactly one solution, so $S$ is a function $F \to H$ .

2.1F1step 1.1algebra

$S$ is linear: if $u_{i} = S (F_{i})$ and $λ$ is a scalar, then for every $v$ , first-slot linearity of $a$ gives $a (u_{1} + u_{2}, v) = F_{1} (v) + F_{2} (v)$ and $a (λ u_{1}, v) = λ F_{1} (v)$ ; by the uniqueness part of [F1], $S (F_{1} + F_{2}) = S (F_{1}) + S (F_{2})$ and $S (λ F_{1}) = λ S (F_{1})$ .

3.1F1F2step 2.1∎

Norm bound: the estimate of [F1] reads $∥ S (F) ∥ \leq ∥ F ∥ / α$ for every $F \in F$ ; hence $S$ is a bounded linear operator with $∥ S ∥ \leq 1 / α$ by [F2]. The same inequality gives $∥ u ∥ \leq ∥ F ∥ / α$ for each datum, uniformly.

Depends on

Used by

Dependency tree · two levels

29 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)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (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)

The Lax--Milgram solution operator has norm at most 1/α1/α