ExampleConstruction: Literature-sourcedVerification: 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.

Complex sesquilinear coercivity differs from bilinear positivity

Example

On $H = C$ define $a (u, v) : = u \overline{v}$ and $b (u, v) : = u v$ . Then $a$ is sesquilinear in the convention of Bounded, coercive and symmetric sesquilinear forms (linear in the first argument, conjugate-linear in the second), bounded with $M = 1$ , and coercive with constant $α = 1$ because $a (u, u) = ∣ u ∣^{2}$ . The expression $b$ is bilinear, not conjugate-linear in the second argument, and it fails the coercivity condition: $b (i, i) = - 1$ , so $Re b (u, u) \geq α ∣ u ∣^{2}$ fails at $u = i$ for every $α > 0$ . More generally $b (u, u) = u^{2}$ is not real for $u \notin R \cup i R$ , and its real part is negative, for example, at $u = 1 + 2 i$ , since $(1 + 2 i)^{2} = - 3 + 4 i$ . Hence the conjugation in the second slot is not cosmetic: the complex Lax--Milgram hypotheses cannot be applied to this bilinear pairing $b$ , and the real bilinear convention of Bounded, coercive and symmetric sesquilinear forms is genuinely a different hypothesis. This tests exactly the convention on which The Lax--Milgram theorem and A bounded form is represented by a unique bounded operator depend, and complements the real-form sources [Si] and [H], which state real bilinear versions.

Facts & Assumptions

Given: The Hilbert space $H = C$ with its usual inner product and $∣ z ∣$ the complex modulus; the pairings $a (u, v) = u \overline{v}$ and $b (u, v) = u v$ .

[F1]

Sesquilinearity, boundedness and coercivity definitions: $a$ is linear in the first slot and conjugate-linear in the second with $∣ a (u, v) ∣ \leq M ∣ u ∣ ∣ v ∣$ , and coercive with constant $α$ when $Re a (u, u) \geq α ∣ u ∣^{2}$ (Bounded, coercive and symmetric sesquilinear forms, Real and complex inner-product spaces and their induced length, Hilbert space).

[F2]

Scalar facts: $u \overline{u} = ∣ u ∣^{2} \geq 0$ , $∣ u \overline{v} ∣ = ∣ u ∣ ∣ v ∣$ , $\overline{i} = - i$ and $i^{2} = - 1$ (Real and imaginary parts, complex conjugation, and modulus).

[F3]

Lax--Milgram and the form-to-operator lemma are stated for sesquilinear forms in the conjugate-linear-second-slot convention (The Lax--Milgram theorem, A bounded form is represented by a unique bounded operator).

Proof

1.1F1F2

The sesquilinear form $a$ : for scalars $λ$ , $a (λ u, v) = λ u \overline{v} = λ a (u, v)$ and $a (u, λ v) = u \overline{λ v} = \overline{λ} a (u, v)$ , so $a$ is linear in the first argument and conjugate-linear in the second; $∣ a (u, v) ∣ = ∣ u ∣ ∣ v ∣ \leq 1 \cdot ∣ u ∣ ∣ v ∣$ gives the bound $M = 1$ , and $a (u, u) = ∣ u ∣^{2}$ gives coercivity with $α = 1$ .

1.2F2F1

The bilinear pairing $b$ is not of this type: $b (λ u, v) = λ b (u, v) = b (u, λ v)$ , so $b$ is bilinear; but with $u = v = 1$ and $λ = i$ , $b (1, i) = i \neq - i = \overline{i} b (1, 1)$ , so $b$ is not conjugate-linear in the second slot.

2.1F2step 1.2algebra

$b$ fails coercivity: $b (i, i) = i^{2} = - 1$ has real part $- 1$ , while $α ∣ i ∣^{2} = α > 0$ for every $α > 0$ ; hence $Re b (u, u) \geq α ∣ u ∣^{2}$ fails at $u = i$ for every $α$ . More generally $b (u, u) = u^{2}$ is not real unless $u \in R \cup i R$ .

3.1F1F2F3step 1.2step 2.1algebra∎

Consequences: neither Lax--Milgram nor the representation lemma applies to this $b$ , since it is not sesquilinear. More generally, a complex form that is both bilinear and sesquilinear satisfies $i c (u, v) = c (u, i v) = - i c (u, v)$ , hence is the zero form. The zero form satisfies the bounded sesquilinear hypotheses of the representation lemma; on a nonzero space it cannot be coercive, but on $H = {0}$ it is coercive with every $α > 0$ and satisfies the Lax--Milgram form hypotheses. Thus the conjugation convention matters, with this zero-form exception.

Depends on

Used by

Nothing in the library uses this result yet.

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

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