LemmaStatement: 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.

A bounded form is represented by a unique bounded operator

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), used through Riesz representation for Hilbert spaces. Let $H$ be a real or complex Hilbert space and let $a$ be a bounded sesquilinear form on $H$ with bound $M$ in the sense of Bounded, coercive and symmetric sesquilinear forms. Then there is a unique bounded linear operator $A \in B (H)$ with $a (u, v) = (A u, v) for all u, v \in H,$ and $∥ A ∥ \leq M$ ; if $M$ is the least bound of $a$ then $∥ A ∥ = M$ . The map $a \mapsto A$ is linear, and $a$ is coercive with constant $α$ if and only if $Re (A u, u) \geq α ∥ u ∥^{2}$ for all $u$ . For the adjoint form one has $a^{*} (u, v) = (A^{*} u, v)$ , where $A^{*}$ is the Hilbert adjoint of The Hilbert-space adjoint of a bounded operator.

Facts & Assumptions

Given: Countable Choice; a real or complex Hilbert space $H$ with inner product $(\cdot, \cdot)$ linear in the first argument and conjugate-linear in the second; a sesquilinear form $a$ on $H$ , linear in the first argument and conjugate-linear in the second, with bound $M \geq 0$ .

[F1]

Bounded and sesquilinear: $a (u, λ v) = \overline{λ} a (u, v)$ , $a (λ u, v) = λ a (u, v)$ , $a (u + u^{'}, v) = a (u, v) + a (u^{'}, v)$ , and $∣ a (u, v) ∣ \leq M ∥ u ∥ ∥ v ∥$ for all $u, v \in H$ (Bounded, coercive and symmetric sesquilinear forms).

[F2]

Inner-product facts: $(v, w) = \overline{(w, v)}$ , positive definiteness (so a vector orthogonal to all of $H$ is $0$ ), and Cauchy--Schwarz $∣ (u, v) ∣ \leq ∥ u ∥ ∥ v ∥$ ; the inner product is linear in the first slot and conjugate-linear in the second (Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, Hilbert space).

[F3]

Riesz representation under Countable Choice: every bounded linear functional $f$ on $H$ has a unique $y \in H$ with $f (x) = (x, y)$ for all $x$ , and $∥ f ∥ = ∥ y ∥$ (Riesz representation for Hilbert spaces, The Axiom of Countable Choice ( ${A C}_{ω}$ ), The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F4]

Bounded operators and the operator norm: $T$ is bounded when some $C \geq 0$ has $∥ T x ∥ \leq C ∥ x ∥$ , and $∥ T ∥ = \sup_{∥ x ∥ \leq 1} ∥ T x ∥$ is its least bound (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[F5]

Hilbert adjoint: there is a unique $A^{*} \in B (H)$ with $(A u, v) = (u, A^{*} v)$ for all $u, v \in H$ (The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

Proof

1.1F1F2

For fixed $u \in H$ the map $f_{u} (v) : = \overline{a (u, v)}$ is linear in $v$ and bounded: $f_{u} (λ v) = \overline{a (u, λ v)} = \overline{\overline{λ} a (u, v)} = λ f_{u} (v)$ and, more generally, conjugate-linearity of $a$ in the second slot makes $f_{u}$ additive, while $∣ f_{u} (v) ∣ = ∣ a (u, v) ∣ \leq M ∥ u ∥ ∥ v ∥$ shows that $∥ f_{u} ∥ \leq M ∥ u ∥$ .

2.1F2F3step 1.1

Riesz representation defines $A$ : by [F3] there is a unique $A u \in H$ with $f_{u} (v) = (v, A u)$ for every $v$ , that is $\overline{a (u, v)} = (v, A u)$ , and $∥ A u ∥ = ∥ f_{u} ∥ \leq M ∥ u ∥$ . Conjugating the representing identity with the conjugate symmetry of the inner product gives $a (u, v) = \overline{(v, A u)} = (A u, v)$ for all $v$ ; so every $u$ is assigned a unique vector $A u$ with $a (u, v) = (A u, v)$ for all $u, v$ , and in particular $∥ A u ∥ \leq M ∥ u ∥$ .

3.1F1F2F4step 2.1

$A$ is linear: for scalars $s, t$ and $u, w \in H$ , first-slot linearity of $a$ gives $a (s u + t w, v) = s a (u, v) + t a (w, v)$ for every $v$ , hence $(A (s u + t w), v) = s (A u, v) + t (A w, v) = (s A u + t A w, v)$ by linearity of the inner product in its first slot, and positive definiteness forces $A (s u + t w) = s A u + t A w$ . Therefore $A$ is linear and, by step 2.1, bounded with $∥ A ∥ \leq M$ .

3.2F2step 2.1

$A$ is unique: if $B \in B (H)$ also satisfies $a (u, v) = (B u, v)$ for all $u, v$ , then $(A u - B u, v) = 0$ for every $v$ , and positive definiteness gives $A u = B u$ for every $u$ , that is $A = B$ . The assignment $a \mapsto A$ is linear: for forms $a, b$ with operators $A, B$ and a scalar $c$ , $(A_{a + c b} u, v) = (a + c b) (u, v) = (A u, v) + c (B u, v) = ((A + c B) u, v)$ for all $v$ , so $A_{a + c b} = A + c B$ by the same uniqueness argument.

4.1F1F2F4step 3.1algebra

Least bound and coercivity: if $M$ is the least bound of $a$ , then for all $u, v \in H$ one has $∣ a (u, v) ∣ = ∣ (A u, v) ∣ \leq ∥ A u ∥ ∥ v ∥ \leq ∥ A ∥ ∥ u ∥ ∥ v ∥$ , so $∥ A ∥$ is itself a bound of $a$ and $M \leq ∥ A ∥$ ; with step 3.1 this gives $∥ A ∥ = M$ . Also, substituting $v = u$ in $a (u, v) = (A u, v)$ gives $a$ coercive with constant $α > 0$ if and only if $Re (A u, u) \geq α ∥ u ∥^{2}$ for every $u$ .

5.1F2F5∎

Adjoint form: for all $u, v \in H$ , $a^{*} (u, v) = \overline{a (v, u)} = \overline{(A v, u)} = (u, A v) = (A^{*} u, v)$ by conjugate symmetry of the inner product and the defining identity $(A v, u) = (v, A^{*} u)$ of the Hilbert adjoint; hence the adjoint form is represented by $A^{*}$ .

Depends on

Used by

Dependency tree · two levels

38 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

Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)
Haim Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations (Springer Universitext, 2011, complete 614-page text) (standard reference, not scraped)