LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Least-squares residual norm is equivalent to H(div) x H1_0 error

Statement

Assume Countable Choice. Let $Ω \subset R^{2}$ be bounded connected Lipschitz and $C_{P}$ satisfy $∥ w ∥_{2} \leq C_{P} ∥ \nabla w ∥_{2}$ on $H_{0}^{1}$ . For $z = (δ σ, δ u) \in H (d i v) \times H_{0}^{1}$ , put $R z = (δ σ + \nabla δ u, d i v δ σ)$ . This is injective and its norm is equivalent to the product graph norm. If $a = ∥ R_{1} z ∥_{2}$ , $b = ∥ R_{2} z ∥_{2}$ , $g = ∥ \nabla δ u ∥_{2}$ , then $g \leq a + C_{P} b$ , $∥ δ u ∥_{2} \leq C_{P} (a + C_{P} b)$ , $∥ δ σ ∥_{2} \leq 2 a + C_{P} b$ , and $∥ R z ∥^{2} \leq 2 ∥ z ∥_{H (d i v) \times H^{1}}^{2}$ .

Facts & Assumptions

Given: Countable Choice, the real spaces and the stated Poincare inequality.

[A1]

Countable Choice is used to choose the H1_0 density sequence in the weak Green passage. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

Residual components follow the least-squares definition. (First-order least-squares formulation of the Dirichlet Poisson problem)

[F2]

H(div) has L2 distributional divergence and graph norm. (The real H(div) space)

[F3]

Homogeneous Dirichlet Poincare holds. (A bounded-domain Poincare inequality for H1-zero fields)

[F4]

H1_0 is the H1 closure of compactly supported smooth functions. (Zero-boundary Sobolev space as a norm closure)

Proof

1.1A1F2F4algebra

Approximate $δ u$ by compactly supported smooth functions. The distributional divergence identity and $L^{2}$ continuity give $(δ σ, \nabla δ u) = - (d i v δ σ, δ u)$ . Substitute $δ σ = R_{1} z - \nabla δ u$ to get $g^{2} = (R_{1} z, \nabla δ u) + (R_{2} z, δ u)$ .

2.1F3step 1.1algebra

Cauchy–Schwarz and [F3] imply $g^{2} \leq a g + C_{P} b g$ . If $g > 0$ , divide by $g$ ; if $g = 0$ , the bound is immediate. Poincare and $δ σ = R_{1} z - \nabla δ u$ give the stated component estimates, controlling the product graph norm.

3.1F1F2step 2.1algebra∎

The first residual square is at most $2 ∥ δ σ ∥_{2}^{2} + 2 ∥ \nabla δ u ∥_{2}^{2}$ and the second is the divergence component. If $R z = 0$ , step 2.1 and Poincare give $δ u = 0$ , then $δ σ = 0$ . This proves reverse boundedness and injectivity.

Depends on

Used by

The conforming RT0/P1 least-squares Poisson minimizer is unique and best approximating Theorem

Dependency tree · two levels

20 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

Peter Bochev and Max Gunzburger, Least-squares finite element methods (standard reference, not scraped)
J. Bond, R. Chaudhry, L. Cyr, and L. Olson, A First-Order System Least-Squares Finite Element Method for the Poisson-Boltzmann Equation (standard reference, not scraped)