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

Piola maps RT and BDM polynomial families onto the physical cell

Statement

For any $d \geq 1$ , write $P_{k}$ for real scalar polynomials of total degree at most $k$ and ${\tilde{P}}_{k}$ for homogeneous scalar polynomials of degree $k$ , including zero, and define the local families ${RT}_{k} = P_{k}^{d} + x {\tilde{P}}_{k}$ and ${BDM}_{k} = P_{k}^{d}$ .

Let $F (\hat{x}) = A \hat{x} + b$ be an orientation-preserving affine bijection between nondegenerate $d$ -simplices, with $J = \det A > 0$ , and use the contravariant Piola map of Contravariant Piola map. For every $k \geq 0$ , it maps ${RT}_{k} (\hat{K})$ bijectively onto ${RT}_{k} (K)$ , and for every $k \geq 1$ it maps ${BDM}_{k} (\hat{K})$ bijectively onto ${BDM}_{k} (K)$ .

Facts & Assumptions

Given: The affine map $F$ , its matrix $A$ , determinant $J > 0$ , and the polynomial families in Affine simplicial meshes and RT/BDM spaces.

[F1]

The Piola push-forward is $(P \hat{v}) (x) = J^{- 1} A \hat{v} (A^{- 1} (x - b))$ , and its inverse is $\hat{v} (\hat{x}) = J A^{- 1} v (A \hat{x} + b)$ . (Contravariant Piola map)

[F2]

The local polynomial formulas in the Statement agree, in dimensions two and three, with the local families in Affine simplicial meshes and RT/BDM spaces. Here they define the notation for all $d \geq 1$ ; no global mesh or domain is needed for this cellwise assertion.

Proof

1.1F1F2algebra

For BDM, if $\hat{v} \in P_{k} (\hat{K})^{d}$ , then $\hat{v} \circ F^{- 1}$ is a vector polynomial of degree at most $k$ in $x$ because $F^{- 1}$ is affine. Multiplication by the constant matrix $J^{- 1} A$ preserves this degree, so [F1] maps BDM into BDM. Applying the same argument to the inverse affine map proves onto-ness.

1.2F1F2algebra

Write an RT field as $\hat{v} (\hat{x}) = \hat{p} (\hat{x}) + \hat{x} \hat{q} (\hat{x})$ with $\hat{p} \in P_{k}^{d}$ and homogeneous $\hat{q}$ of degree $k$ . The push-forward of the first term is in $P_{k}^{d}$ . For the second term, use $\hat{x} = A^{- 1} (x - b)$ : its image is $J^{- 1} (x - b) \hat{q} (A^{- 1} (x - b))$ . The degree- $k$ homogeneous part of $\hat{q} (A^{- 1} (x - b))$ is $q_{k} (x) : = \hat{q} (A^{- 1} x)$ , with remainder of degree at most $k - 1$ (zero when $k = 0$ ). Thus $(x - b) \hat{q} (A^{- 1} (x - b)) = x q_{k} (x) + p_{k} (x)$ for some vector polynomial $p_{k}$ of degree at most $k$ : all terms from $x$ times the remainder and from $b$ times the full scalar polynomial have degree at most $k$ . Therefore the image lies in ${RT}_{k} (K)$ .

2.1F1step 1.2algebra∎

The inverse Piola map is the contravariant Piola map for the orientation-preserving affine bijection $F^{- 1}$ , up to the displayed inverse formula in [F1]. The same polynomial decomposition from step 1.2 applied to $F^{- 1}$ maps ${RT}_{k} (K)$ into ${RT}_{k} (\hat{K})$ . Hence the forward inclusion is onto.

Depends on

Used by

Dependency tree · two levels

7 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 III Chapter 14: H(div) finite elements (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)