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 coercive form operator is bounded below

Statement

Assume Countable Choice, used through A bounded form is represented by a unique bounded operator. Let $a$ be a bounded coercive sesquilinear form on a real or complex Hilbert space $H$ with constants $M, α$ (Bounded, coercive and symmetric sesquilinear forms) and let $A$ be its operator, $a (u, v) = (A u, v)$ . Then $α ∥ u ∥ \leq ∥ A u ∥ \leq M ∥ u ∥ for every u \in H,$ so $A$ is injective and bounded below with constant $α$ in the sense of A bounded operator that is bounded below.

Facts & Assumptions

Given: Countable Choice; a real or complex Hilbert space $H$ ; a bounded coercive sesquilinear form $a$ on $H$ with bound $M \geq 0$ and coercivity constant $α > 0$ ; and its operator $A \in B (H)$ , $a (u, v) = (A u, v)$ .

[F1]

$A$ exists, is linear and bounded with $a (u, v) = (A u, v)$ for all $u, v$ and $∥ A ∥ \leq M$ ; $a$ is linear in the first argument and conjugate-linear in the second, and $Re a (u, u) \geq α ∥ u ∥^{2}$ (Bounded, coercive and symmetric sesquilinear forms, A bounded form is represented by a unique bounded operator).

[F2]

Cauchy--Schwarz: $∣ (x, y) ∣ \leq ∥ x ∥ ∥ y ∥$ ; and for a complex number $z$ one has $Re z \leq ∣ z ∣$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, Real and imaginary parts, complex conjugation, and modulus).

[F3]

$T \in B (X, Y)$ is bounded below when $∥ T x ∥ \geq c ∥ x ∥$ for all $x$ and some $c > 0$ ; $∥ A ∥ = \sup_{∥ x ∥ \leq 1} ∥ A x ∥$ is a bound for $A$ (A bounded operator that is bounded below, The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Proof

1.1F1F2algebra

Lower bound: for every $u \in H$ the coercivity of $a$ and the identity $a (u, u) = (A u, u)$ give $α ∥ u ∥^{2} \leq Re a (u, u) = Re (A u, u) \leq ∣ (A u, u) ∣ \leq ∥ A u ∥ ∥ u ∥ .$ If $u \neq 0$ divide by $∥ u ∥$ ; if $u = 0$ both sides vanish. Hence $α ∥ u ∥ \leq ∥ A u ∥$ for every $u \in H$ .

1.2F1F3

Upper bound: $∥ A u ∥ \leq ∥ A ∥ ∥ u ∥ \leq M ∥ u ∥$ for every $u$ , since $∥ A ∥ \leq M$ .

2.1F1F3step 1.1step 1.2∎

Consequences: by step 1.1, $A u = 0$ forces $α ∥ u ∥ \leq 0$ , hence $∥ u ∥ = 0$ and $u = 0$ , so $A$ is injective; together with step 1.1 this says exactly that $A$ is bounded below with constant $α$ , while step 1.2 supplies the upper bound, so $α ∥ u ∥ \leq ∥ A u ∥ \leq M ∥ u ∥$ for every $u \in H$ .

Depends on

Used by

Dependency tree · two levels

31 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

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