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.

Coercivity makes a small form step a strict contraction

Statement

Assume Countable Choice, used through A bounded form is represented by a unique bounded operator. Let $H \neq {0}$ be a real or complex Hilbert space and let $a$ be a bounded coercive sesquilinear form on $H$ with constants $M > 0, α > 0$ (so necessarily $α \leq M$ ); let $A$ be its operator. Put $q_{ρ} : = \sqrt{1 - 2 ρ α + ρ^{2} M^{2}}$ for $0 < ρ < 2 α / M^{2}$ . Then $0 \leq q_{ρ} < 1$ , and for every $w \in H$ the map $T_{ρ, w} (u) : = u - ρ (A u - w)$ is a strict contraction of $H$ with constant $q_{ρ}$ : $∥ T_{ρ, w} (u) - T_{ρ, w} (v) ∥ \leq q_{ρ} ∥ u - v ∥$ for all $u, v$ . In particular $I - ρ A$ is a strict contraction with the same constant. The estimate is the only place where the coercivity constant and the bound enter the contraction argument.

Facts & Assumptions

Given: Countable Choice; a Hilbert space $H \neq {0}$ with inner product linear in the first argument; a bounded coercive sesquilinear form $a$ with constants $M > 0, α > 0$ ; its operator $A$ , $a (u, v) = (A u, v)$ ; and a real $ρ$ with $0 < ρ < 2 α / M^{2}$ .

[F1]

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

[F2]

Inner-product norm expansion: $∥ z - ρ A z ∥^{2} = ∥ z ∥^{2} - 2 ρ Re (A z, z) + ρ^{2} ∥ A z ∥^{2}$ , and $Re (A z, z) \leq ∣ (A z, z) ∣ \leq ∥ A z ∥ ∥ z ∥$ by Cauchy--Schwarz; the induced length is a norm with the triangle inequality (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs, The induced length is a norm, Real and imaginary parts, complex conjugation, and modulus).

[F3]

A map $S : H \to H$ is a strict contraction with constant $q$ when $∥ S (u) - S (v) ∥ \leq q ∥ u - v ∥$ for all $u, v$ and $0 \leq q < 1$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction).

[F4]

Nonnegative square roots: for $t \geq 0$ there is a unique $s \geq 0$ with $s^{2} = t$ , denoted $\sqrt{t}$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ). If $0 \leq x \leq y$ , then $\sqrt{x} > \sqrt{y}$ would imply $x - y = (\sqrt{x} - \sqrt{y}) (\sqrt{x} + \sqrt{y}) > 0$ , a contradiction; hence $\sqrt{x} \leq \sqrt{y}$ .

Proof

1.1F1algebra

On a nonzero Hilbert space the named constants satisfy $α \leq M$ : choosing $u \neq 0$ and dividing $u$ by its norm, $α \leq Re a (u, u) \leq ∣ a (u, u) ∣ \leq M ∥ u ∥^{2} = M$ , The identity $1 - 2 ρ α + ρ^{2} M^{2} = M^{2} (ρ - α / M^{2})^{2} + 1 - α^{2} / M^{2}$ makes the radicand nonnegative; it may vanish when $α = M$ and $ρ = α / M^{2}$ .

1.2F1F2algebra

Contraction estimate: for $z \in H$ and $0 < ρ < 2 α / M^{2}$ the expansion of [F2] together with [F1] gives $∥ z - ρ A z ∥^{2} = ∥ z ∥^{2} - 2 ρ Re (A z, z) + ρ^{2} ∥ A z ∥^{2} \leq (1 - 2 ρ α + ρ^{2} M^{2}) ∥ z ∥^{2} = q_{ρ}^{2} ∥ z ∥^{2},$ so $∥ (I - ρ A) z ∥ \leq q_{ρ} ∥ z ∥$ ; taking $z = u - v$ and using $T_{ρ, w} (u) - T_{ρ, w} (v) = (I - ρ A) (u - v)$ gives the contraction estimate for every $w$ .

2.1F3F4step 1.1step 1.2algebra∎

The constant lies in $[0, 1)$ : the radicand is a quadratic in $ρ$ with minimum $1 - α^{2} / M^{2}$ at $ρ = α / M^{2}$ , which is nonnegative because $α \leq M$ by step 1.1; at the endpoints $ρ = 0$ and $ρ = 2 α / M^{2}$ it equals $1$ , and for $0 < ρ < 2 α / M^{2}$ either directly $1 - 2 ρ α + ρ^{2} M^{2} < 1$ or by the strict minimum unless $ρ = α / M^{2}$ and $α = M$ , in which case the radicand vanishes and $q_{ρ} = 0$ ; in every case $0 \leq q_{ρ} < 1$ . Hence $I - ρ A$ , and with it $T_{ρ, w}$ , is a strict contraction with constant $q_{ρ}$ .

Depends on

Used by

The Lax--Milgram theorem Theorem

Dependency tree · two levels

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