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.

Discrete gradient gap from a relative commuting projection

Statement

Assume AC. Let $Ω \subset R^{3}$ be nonempty, bounded, and open. Write $H = L^{2} (Ω; R^{3})$ , $B = \nabla H_{0}^{1} (Ω)$ , and let $P_{B}$ denote the $H$ -orthogonal projection onto $B$ . Let $S_{h} \subset H_{0}^{1} (Ω)$ and $V_{h} \subset H_{0} (curl; Ω)$ be finite-dimensional subspaces with $B_{h} = \nabla S_{h} \subset V_{h}$ . Suppose linear projections $Π_{h}^{0} : H_{0}^{1} \to S_{h}$ and $Π_{h}^{1} : H_{0} (curl) \to V_{h}$ satisfy $Π_{h}^{1} \nabla = \nabla Π_{h}^{0}$ . For $v_{h} \in V_{h} \cap B_{h}^{⊥}$ , put $w_{h} = (I - P_{B}) v_{h}$ . Then $w_{h} \in H_{0} (curl) \cap B^{⊥}$ , $curl w_{h} = curl v_{h}$ , and $∥ v_{h} - w_{h} ∥_{2} \leq ∥ Π_{h}^{1} w_{h} - w_{h} ∥_{2} .$ If moreover $\sup_{h} ∥ Π_{h}^{1} ∥_{H \to H} \leq M$ and $Π_{h}^{1} f \to f$ in $H$ for each fixed $f \in H_{0} (curl)$ , every $H$ -convergent sequence of lifts $w_{h}$ has $∥ v_{h} - w_{h} ∥_{2} \to 0$ . Here the $H$ operator norm means that the graph-space operators possess bounded extensions to $H$ .

Facts & Assumptions

Given: AC, the spaces and relative commuting projections in the Statement. When the domain and mesh satisfy the projection theorem's hypotheses, its separate homogeneous family supplies a concrete instance of these relative-degree-zero, $L^{2}$ -boundedness and strong-convergence interfaces. The present result is conditional only on the abstract projection hypotheses in its own Statement, and the unrestricted family is not used here.

[F1]

On bounded open sets, the scalar zero-boundary Poincare inequality holds under CC. (The Poincare inequality for zero-boundary Sobolev closures on domains bounded in one direction, The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F2]

A nonempty closed convex subset of a real Hilbert space has a unique nearest point under CC, characterized by the variational inequality. (Projection onto a nonempty closed convex set, Variational characterisation of the nearest point)

[F3]

Sobolev spaces are complete under AC; $H_{0}^{1}$ is a closed subspace by its closure definition. Real $L^{2}$ is Hilbert under CC, and compactly supported smooth functions are dense in $L^{2}$ on every open set under CC, applied in each of three components. (Integer-order Sobolev spaces are Banach, $L^{2}$ with the integral pairing is a Hilbert space, Smooth compactly supported functions of an open set are dense in $L^{2}$ )

[A1]

AC implies the CC used in [F1] and [F2]. (The Axiom of Choice)

Proof

1.1F1F2F3A1givenconstruct

If $\nabla p_{n}$ is Cauchy in $H$ , [F1] makes $p_{n}$ Cauchy in $H_{0}^{1}$ , so its limit $p \in H_{0}^{1}$ has $\nabla p_{n} \to \nabla p$ . Thus $B$ is closed. Apply [F2] to $B$ . For its nearest point $P_{B} v$ , testing the variational inequality with $P_{B} v \pm b$ , $b \in B$ , gives $v - P_{B} v ⊥ B$ . Uniqueness of this decomposition proves linearity, and its Pythagorean identity proves that $P_{B}$ and $I - P_{B}$ are contractions. Finally, if $p \in H_{0}^{1}$ , smooth compactly supported approximation shows $\nabla p \in H_{0} (curl)$ with curl zero: convergence of the gradients is convergence in the curl graph norm. Therefore $w_{h} = v_{h} - P_{B} v_{h}$ has the stated membership and curl.

2.1step 1.1givenalgebra

Write $v_{h} - w_{h} = \nabla p_{h}$ with $p_{h} \in H_{0}^{1}$ , and put $e_{h} = v_{h} - Π_{h}^{1} w_{h}$ . Identity on $V_{h}$ and commutation give $e_{h} = Π_{h}^{1} (v_{h} - w_{h}) = \nabla Π_{h}^{0} p_{h} \in B_{h}$ . Both $v_{h}$ and $w_{h}$ are orthogonal to $B_{h}$ , hence $(v_{h} - w_{h}, e_{h}) = 0$ . Since $v_{h} - w_{h} = e_{h} + (Π_{h}^{1} w_{h} - w_{h})$ , Cauchy–Schwarz yields $∥ v_{h} - w_{h} ∥_{2}^{2} = (v_{h} - w_{h}, Π_{h}^{1} w_{h} - w_{h}) \leq ∥ v_{h} - w_{h} ∥_{2} ∥ Π_{h}^{1} w_{h} - w_{h} ∥_{2}$ . Division if the left factor is nonzero proves the inequality; the zero case is immediate. This is the missing discrete-gradient estimate.

3.1F3step 2.1givenalgebra∎

Suppose $w_{h} \to w$ in $H$ . The $L^{2}$ extensions of the projections converge strongly to identity on all $H$ : first approximate an arbitrary $f \in H$ by a smooth compactly supported vector field $g$ , then use $∥ (I - Π_{h}^{1}) f ∥_{2} \leq (1 + M) ∥ f - g ∥_{2} + ∥ (I - Π_{h}^{1}) g ∥_{2}$ . Consequently $∥ Π_{h}^{1} w_{h} - w_{h} ∥_{2} \leq (1 + M) ∥ w_{h} - w ∥_{2} + ∥ Π_{h}^{1} w - w ∥_{2} \to 0$ . Step 2.1 gives the last assertion.

Depends on

Used by

Discrete compactness and uniform Poincare inequality for Nedelec fields Theorem

Dependency tree · two levels

72 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

Douglas N. Arnold, Richard S. Falk, and Ragnar Winther, Finite element exterior calculus: from Hodge theory to numerical stability (standard reference, not scraped)