LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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.

Face averages are unisolvent for the local Crouzeix–Raviart element

Statement

For the element of The local P1 Crouzeix–Raviart element, the face-average functionals form an isomorphism $P_{1} (K) \to R^{d + 1}$ . In particular, $\frac{1}{∣ F_{j} ∣} \int_{F_{j}} ϕ_{K, F_{i}} d S = δ_{i j}, ϕ_{K, F_{i}} = 1 - d λ_{i},$ so every $p \in P_{1} (K)$ has the unique expansion $p = \sum_{i = 0}^{d} σ_{K, F_{i}} (p) ϕ_{K, F_{i}}$ .

Facts & Assumptions

Given: A nondegenerate affine $d$ -simplex $K$ , its facets $F_{i}$ , barycentric coordinates $λ_{i}$ , and the face-average functionals and candidate shape polynomials of The local P1 Crouzeix–Raviart element.

[F1]

The barycentric coordinates are affine, satisfy $λ_{i} (a_{j}) = δ_{i j}$ , and sum to one on $K$ . (The local P1 Crouzeix–Raviart element)

[F2]

The average of an affine function over a simplex facet equals its value at that facet's barycenter; this follows by integrating each affine coordinate in the affine parametrization of the facet. (The local P1 Crouzeix–Raviart element)

Proof

1.1F1F2givenalgebra

Let $b_{j}$ be the barycenter of $F_{j}$ . By [F2], the face average of an affine polynomial $p$ on $F_{j}$ is $p (b_{j})$ . At $b_{j}$ , the barycentric coordinates of the $d$ vertices of $F_{j}$ are all $1 / d$ , while the coordinate opposite $F_{j}$ is zero. Therefore $λ_{i} (b_{j}) = 0$ if $i = j$ and $λ_{i} (b_{j}) = 1 / d$ if $i \neq j$ . Hence $(1 - d λ_{i}) (b_{j}) = δ_{i j}$ , which proves the displayed duality identities.

2.1step 1.1algebra∎

The $d + 1$ polynomials $ϕ_{K, F_{i}}$ are linearly independent: applying $σ_{K, F_{j}}$ to $\sum_{i} c_{i} ϕ_{K, F_{i}} = 0$ gives $c_{j} = 0$ by step 1.1. Since $P_{1} (K)$ has dimension $d + 1$ , they form a basis. Applying the same functionals to $p - \sum_{i} σ_{K, F_{i}} (p) ϕ_{K, F_{i}}$ gives zero for every face; expansion in this basis then gives zero coefficients. This proves existence and uniqueness of the stated expansion.

Depends on

The local P1 Crouzeix–Raviart element

Used by

Dependency tree · two levels

3 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)