TheoremStatement: 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.

Well-posedness of the homogeneous Poisson and CR problems

Statement

Assume Countable Choice, let $Ω$ and $T_{h}$ be as in The Crouzeix–Raviart method for the homogeneous Poisson problem, and let $f \in L^{2} (Ω)$ . The exact weak problem has a unique solution $u \in H_{0}^{1} (Ω)$ , and the discrete problem has a unique solution $u_{h} \in V_{h}^{C R, 0}$ . The exact existence argument uses Countable Choice through Hilbert-space structure and Lax–Milgram. The finite-dimensional discrete existence and uniqueness argument uses no choice principle.

Facts & Assumptions

Given: Countable Choice, the bounded domain and mesh of The Crouzeix–Raviart method for the homogeneous Poisson problem, $f \in L^{2} (Ω)$ , and a slab $a < x \cdot e < b$ containing $Ω$ for some unit vector $e$ . Throughout, the datum and the Sobolev and $L^{2}$ spaces are real-valued, consistently with the real affine polynomials defining the CR space.

[F1]

$H_{0}^{1} (Ω)$ is a Hilbert space under its $H^{1}$ inner product; the $L^{2}$ load is bounded when controlled by the $L^{2}$ norm. (The Sobolev space $H^{1}$ is a Hilbert space, Holder's inequality for integrals, including the endpoint cases)

[F2]

The continuous Poincare inequality controls $∥ v ∥_{2}$ by $∥ \nabla v ∥_{2}$ on $H_{0}^{1} (Ω)$ . (A Poincare bound on a slab-bounded domain)

[F3]

Lax–Milgram gives a unique exact solution for a bounded coercive form and bounded load on a Hilbert space under Countable Choice. (The Lax--Milgram theorem)

[F4]

$V_{h}^{C R, 0}$ has a finite basis indexed by interior facets. (Interior face means form the global Crouzeix–Raviart degrees of freedom)

[F5]

$∥ \nabla_{h} \cdot ∥_{2}$ is a norm on $V_{h}^{C R, 0}$ . (The broken gradient is a norm on the homogeneous Crouzeix–Raviart space)

Proof

1.1F1F2F3givenalgebra

Let $V = H_{0}^{1} (Ω)$ with its $H^{1}$ Hilbert norm. For $v, w \in V$ , $∣ a (v, w) ∣ \leq ∥ \nabla v ∥_{2} ∥ \nabla w ∥_{2} \leq ∥ v ∥_{H^{1}} ∥ w ∥_{H^{1}} .$ By [F2], $∥ v ∥_{H^{1}}^{2} = ∥ v ∥_{2}^{2} + ∥ \nabla v ∥_{2}^{2} \leq (1 + C_{P}^{2}) ∥ \nabla v ∥_{2}^{2}$ , so $a (v, v) \geq (1 + C_{P}^{2})^{- 1} ∥ v ∥_{H^{1}}^{2}$ . Also $∣ F (v) ∣ \leq ∥ f ∥_{2} ∥ v ∥_{2} \leq C_{P} ∥ f ∥_{2} ∥ v ∥_{H^{1}}$ . Thus [F3] gives a unique exact weak solution.

2.1F1F4F5givenalgebra∎

By [F4], write the finite-dimensional space in its explicit face basis. The matrix of $a_{h}$ in this basis is positive definite: for any coefficient vector $c$ , its quadratic form is $∥ \nabla_{h} \sum_{F} c_{F} ϕ_{F} ∥_{2}^{2}$ , which vanishes only for the zero coefficient vector by [F5] and basis independence. Hence the matrix is invertible by finite-dimensional linear algebra. The load vector has finite entries because every basis function is piecewise affine and in $L^{2}$ , so Holder [F1] gives $∣ F_{h} (ϕ_{F}) ∣ \leq ∥ f ∥_{2} ∥ ϕ_{F} ∥_{2}$ . Solving the finite linear system gives exactly one $u_{h}$ . If there are no interior facets, the space is zero and its unique element $u_{h} = 0$ solves the vacuous equations. This discrete argument is the explicit face-basis matrix solve; [F3] is used only for the exact continuous problem in step 1.1. Thus the discrete proof itself makes no choice.

Depends on

Used by

Energy error estimate for the Crouzeix–Raviart Poisson method Theorem

Dependency tree · two levels

56 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

Jean-Luc Guermond, MATH 661 Fall 2025, Part VIII, Chapter 36, Crouzeix–Raviart approximation (standard reference, not scraped)
Joachim Schöberl, Numerical Methods for Partial Differential Equations, Chapter 25, Non-conforming Finite Element Methods (standard reference, not scraped)