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.

The adjoint of a coercive form is coercive with the same constants

Statement

Assume Countable Choice, used through the Riesz representation and Hilbert-adjoint suppliers. Let $a$ be a bounded sesquilinear form on a real or complex Hilbert space with bound $M$ and coercivity constant $α > 0$ (Bounded, coercive and symmetric sesquilinear forms), and let $a^{*} (u, v) : = \overline{a (v, u)}$ . Then $a^{*}$ is bounded with the same bound $M$ and coercive with the same constant $α$ ; its operator is the Hilbert adjoint $A^{*}$ of the operator $A$ of $a$ (A bounded form is represented by a unique bounded operator). In particular $\ker A^{*} = {0}$ and $(ran A)^{⊥} = \ker A^{*}$ , so the range of $A$ is dense in the classical route to surjectivity.

Facts & Assumptions

Given: Countable Choice; a real or complex Hilbert space $H$ ; a bounded sesquilinear form $a$ with bound $M \geq 0$ and coercivity constant $α > 0$ ; the adjoint form $a^{*} (u, v) = \overline{a (v, u)}$ ; and the operator $A$ of $a$ , $a (u, v) = (A u, v)$ .

[F1]

$a$ is linear in the first argument and conjugate-linear in the second, with $∣ a (u, v) ∣ \leq M ∥ u ∥ ∥ v ∥$ and $Re a (u, u) \geq α ∥ u ∥^{2}$ (Bounded, coercive and symmetric sesquilinear forms).

[F2]

The operator $A$ exists, is linear and bounded with $a (u, v) = (A u, v)$ , and $a^{*} (u, v) = (A^{*} u, v)$ where $A^{*}$ is the Hilbert adjoint of $A$ ; moreover the adjoint form $a^{*}$ is again a sesquilinear form (A bounded form is represented by a unique bounded operator, The Hilbert-space adjoint of a bounded operator, Hilbert-adjoint identities).

[F3]

A bounded coercive form's operator is bounded below with the coercivity constant: for the form $a^{*}$ with operator $A^{*}$ this gives $α ∥ u ∥ \leq ∥ A^{*} u ∥$ (A coercive form operator is bounded below).

[F4]

Kernel--range orthogonality: $(ran A)^{⊥} = \ker A^{*}$ and $\overline{ran A} = (\ker A^{*})^{⊥}$ for the Hilbert adjoint (Kernel–range orthogonality for Hilbert adjoints, The Hilbert-space adjoint of a bounded operator).

[F5]

Conjugation is an involution with $Re \overline{z} = Re z$ and $∣ z ∣ = ∣ \overline{z} ∣$ (Real and imaginary parts, complex conjugation, and modulus, Real and complex inner-product spaces and their induced length).

Proof

1.1F1F2F5

Boundedness of $a^{*}$ : for all $u, v \in H$ , $∣ a^{*} (u, v) ∣ = ∣ \overline{a (v, u)} ∣ = ∣ a (v, u) ∣ \leq M ∥ v ∥ ∥ u ∥$ , so $a^{*}$ is bounded with the same bound $M$ ; it is sesquilinear of the same type, being conjugate-linear in $v$ and linear in $u$ .

1.2F1F5algebra

Coercivity of $a^{*}$ : $a^{*} (u, u) = \overline{a (u, u)}$ has the same real part as $a (u, u)$ , hence $Re a^{*} (u, u) = Re a (u, u) \geq α ∥ u ∥^{2}$ for every $u$ .

2.1F2F3step 1.2

Operator and kernel: [F2] identifies the operator of $a^{*}$ as the Hilbert adjoint $A^{*}$ ; since $a^{*}$ is bounded and coercive with constant $α$ , [F3] gives $α ∥ u ∥ \leq ∥ A^{*} u ∥$ , so $A^{*} u = 0$ forces $u = 0$ , that is $\ker A^{*} = {0}$ .

3.1F4step 2.1∎

Orthogonality: by [F4], $(ran A)^{⊥} = \ker A^{*} = {0}$ , so the orthogonal complement of the range of $A$ is trivial and $\overline{ran A} = (\ker A^{*})^{⊥} = H$ ; the range of $A$ is dense.

Depends on

Used by

Dependency tree · two levels

35 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)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (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)