CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Weak well-posedness for constant divergence-free convection

Statement

Assume Countable Choice as in the cited Sobolev and Lax–Milgram suppliers. Let $Ω \subset R^{2}$ be a bounded polygon, $b \in R^{2}$ constant, and $f \in L^{2} (Ω; R)$ . Here $H_{0}^{1}$ is the zero-boundary closure of Zero-boundary Sobolev space as a norm closure. There is a unique real-valued $u \in H_{0}^{1} (Ω; R)$ satisfying $\int_{Ω} \nabla u \cdot \nabla v + (b \cdot \nabla u) v d x = \int_{Ω} f v d x (v \in H_{0}^{1} (Ω)) .$ No $H^{2}$ regularity is asserted.

Facts & Assumptions

[A1]

Countable Choice is assumed for the cited Sobolev, Poincare and Lax–Milgram interfaces (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Given: Countable Choice, a bounded polygon $Ω$ , constant $b$ , $f \in L^{2} (Ω)$ , and the real Hilbert space $H_{0}^{1} (Ω)$ .

[F1]

On a domain bounded in one direction, $∥ v ∥_{L^{2}} \leq C_{P} ∥ \nabla v ∥_{L^{2}}$ for every $v \in H_{0}^{1}$ ; the supplier assumes Countable Choice (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

The real bounded coercive (not necessarily symmetric) Lax–Milgram theorem assumes Countable Choice and gives a unique variational solution for every bounded linear functional (The Lax--Milgram theorem, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F3]

$W^{1, 2}$ is a Hilbert space under its Sobolev inner product; its zero-boundary closure is closed, and Poincare makes the gradient norm equivalent to the inherited norm (The Sobolev space $H^{1}$ is a Hilbert space, Hilbert space, Zero-boundary Sobolev space as a norm closure, The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction).

Proof

1.1A1F1F3givenalgebra

A bounded polygon lies in a finite-width slab, so [F1] applies. Define $a (w, v) = \int \nabla w \cdot \nabla v + (b \cdot \nabla w) v$ . Cauchy–Schwarz and [F1] give $∣ a (w, v) ∣ \leq (1 + ∣ b ∣ C_{P}) ∥ \nabla w ∥_{2} ∥ \nabla v ∥_{2}$ ; also $F (v) = \int f v$ is linear and $∣ F (v) ∣ \leq C_{P} ∥ f ∥_{2} ∥ \nabla v ∥_{2}$ . The gradient norm is complete on $H_{0}^{1}$ by [F3], since Poincare makes it equivalent to the complete inherited $H^{1}$ norm.

1.2A1F1F3givenalgebra

For $w \in C_{c}^{\infty} (Ω)$ , $\int (b \cdot \nabla w) w = \frac{1}{2} \int b \cdot \nabla (w^{2}) = 0$ by compact support and constant $b$ . Approximation in $H_{0}^{1}$ extends this identity to every $w \in H_{0}^{1}$ , because $w \mapsto \int (b \cdot \nabla w) w$ is continuous in the $H^{1}$ norm and compactly supported smooth functions are dense by [F3]. Hence $a (w, w) = ∥ \nabla w ∥_{2}^{2}$ , so $a$ is coercive with constant $1$ in the gradient norm.

2.1A1F1F2F3step 1.1step 1.2∎

Apply [F2] to the real Hilbert space $H_{0}^{1} (Ω)$ equipped with inner product $(w, v)_{H} = \int \nabla w \cdot \nabla v$ , the bounded form from step 1.1, and its coercivity from step 1.2. This gives a unique $u$ satisfying $a (u, v) = F (v)$ for all $v$ . These are exactly the displayed weak equations. Countable Choice is inherited from [F1], [F2] and [F3]; no full Axiom of Choice or elliptic regularity is used.

Depends on

Used by

Linear contraction of AFEM energy error and oscillation Theorem

Dependency tree · two levels

62 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

Ricardo H. Nochetto, Adaptive Finite Element Methods, Lecture 3 (standard reference, not scraped)
Cascón, Kreuzer, Nochetto & Siebert, Quasi-optimal convergence rate for an AFEM (standard reference, not scraped)
Bonito, Canuto, Nochetto & Veeser, Adaptive Finite Element Methods (2024) (standard reference, not scraped)