Finite element method. Detailed proofs to be formalized in Coq

TL;DR

This work develops a rigorous, formally verifiable foundation for the finite element method, focusing on Lagrange finite elements on simplices and their unisolvence. It defines FEM as a triple (K, P, Σ), and builds the theory from affine geometry, reference elements, and multi-indexed polynomial spaces P^d_k, culminating in detailed sketches and then full proofs (via Part II) of unisolvence and related properties. The document emphasizes constructive, pen-and-paper proofs aligned with Coq formalization, linking classical FEM concepts to algebraic and geometric tools (e.g., barycentric coordinates, affine maps, and multivariate polynomials) while acknowledging practical non-affine extensions. The approach aims to certify numerical FEM implementations, accounting for interpolation, mesh mappings, and node configurations, with a view toward future full formalization and broader applicability in PDE numerics.

Abstract

To obtain the highest confidence on the correction of numerical simulation programs for the resolution of Partial Differential Equations (PDEs), one has to formalize the mathematical notions and results that allow to establish the soundness of the approach. The finite element method is one of the popular tools for the numerical resolution of a wide range of PDEs. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs for the construction of the Lagrange finite elements of any degree on simplices in positive dimension.

Figures (17)

• Figure 1: Brief recall of the various components of a typical (stationary) FEM formulation. The black thick arrows depict the usual construction steps when solving a problem via the FEM. The black thick dashed arrow shows the possible feedback loop that a posteriori analysis allows, to change the mesh, the finite element (i.e. the order of polynomial approximation, the quadrature formula or the numerical scheme). The red dashed arrows depict when a theorem or a numerical tool takes place.
• Figure 2: Lagrange nodes ${{\{\space\{\hat{{\bf a}}\}\space\}}_{\!{\mathcal{A}}^d_k}}$ of the reference simplex $\hat{K}_d$ when $d\in\{2,3\}$ and $k=3$ (see Section \ref{['ss:multi-ind-fem']}). Each node is depicted as a colored ball, and corresponds to a unique element of ${\mathcal{A}}^d_3$. The colors correspond to degrees $l\leqslant3$ of polynomials, or equivalently to lengths of multi-indices (i.e. in $\mathcal{C}^d_{l}$ for $l\leqslant3$). In magenta, the node $\hat{{\bf a}}_{\bf 0}$ corresponds to constant polynomials (with degree 0) in $\mathbb{P}^d_{0}$, and to the multi-index ${\bf 0}$ in the singleton $\mathcal{C}^d_{0}$. In green, the nodes correspond to non-constant affine polynomials (with degree 1), and to the multi-indices ${\bf e}_1,\ldots,{\bf e}_d$ in $\mathcal{C}^d_{1}$. In red, the nodes correspond to non-affine quadratic polynomials (with degree 2), and to multi-indices in $\mathcal{C}^d_{2}$. In blue, the nodes correspond to non-quadratic cubic polynomials (with degree 3), and to multi-indices in $\mathcal{C}^d_{3}$. We observe in this picture that ${\mathcal{A}}^d_3=\mathcal{C}^d_{0}\uplus\mathcal{C}^d_{1}\uplus\mathcal{C}^d_{2}\uplus\mathcal{C}^d_{3}$.
• Figure 3: Lex (top left), colex (top right), symlex (bottom left), and revlex (bottom right) orderings of ${\mathcal{A}}^d_k$ when $d=2$ and $k=3$ (see Section \ref{['ss:lex']}). The increase in the order is represented by dashed arrows. For ${\mathcal{A}}^2_3$, we have $(0,0)<^{\mathrm{lex}}(0,1)<^{\mathrm{lex}}(0,2)<^{\mathrm{lex}}(0,3)<^{\mathrm{lex}}(1,0)<^{\mathrm{lex}}(1,1)<^{\mathrm{lex}}(1,2)<^{\mathrm{lex}}(2,0)<^{\mathrm{lex}}(2,1)<^{\mathrm{lex}}(3,0)$, and $(0,0)<^{\mathrm{colex}}(1,0)<^{\mathrm{colex}}(2,0)<^{\mathrm{colex}}(3,0)<^{\mathrm{colex}}(0,1)<^{\mathrm{colex}}(1,1)<^{\mathrm{colex}}(2,1)<^{\mathrm{colex}}(0,2)<^{\mathrm{colex}}(1,2)<^{\mathrm{colex}}(0,3)$. The symlex order is the symmetrical of the lex order, and the revlex order is the symmetrical of the colex order. For instance, when the length is 3 (hypotenuse of the triangles, blue nodes), we have $(0,3)<^{\mathrm{lex}}(1,2)<^{\mathrm{lex}}(2,1)<^{\mathrm{lex}}(3,0)$, and also $(0,3)<^{\mathrm{revlex}}(1,2)<^{\mathrm{revlex}}(2,1)<^{\mathrm{revlex}}(3,0)$.
• Figure 4: Grlex (or deglex) ordering of ${\mathcal{A}}^d_k$ when $d\in\{2,3\}$ and $k=3$ (see Section \ref{['ss:grlex']}). The increase in the order is represented by dashed arrows (only in the case $l=3$ when $d=3$, see Figure \ref{['f:lag-k3-d2-d3']}). For ${\mathcal{A}}^2_3$ ($d=2$), we have $(0,0)<^{\mathrm{grlex}}(0,1)<^{\mathrm{grlex}}(1,0)<^{\mathrm{grlex}}(0,2)<^{\mathrm{grlex}}(1,1)<^{\mathrm{grlex}}(2,0)<^{\mathrm{grlex}}(0,3)<^{\mathrm{grlex}}(1,2)<^{\mathrm{grlex}}(2,1)<^{\mathrm{grlex}}(3,0)$. For $\mathcal{C}^3_3$ ($d=3$), we have $(0,0,3)<^{\mathrm{grlex}}(0,1,2)<^{\mathrm{grlex}}(0,2,1)<^{\mathrm{grlex}}(0,3,0)<^{\mathrm{grlex}}(1,0,2)<^{\mathrm{grlex}}(1,1,1)<^{\mathrm{grlex}}(1,2,0)<^{\mathrm{grlex}}(2,0,1)<^{\mathrm{grlex}}(2,1,0)<^{\mathrm{grlex}}(3,0,0)$.
• Figure 5: Grcolex ordering of ${\mathcal{A}}^d_k$ when $d\in\{2,3\}$ and $k=3$ (see Section \ref{['ss:grcolex']}). The increase in the order is represented by dashed arrows (only in the case $l=3$ when $d=3$, see Figure \ref{['f:lag-k3-d2-d3']}). For ${\mathcal{A}}^2_3$ ($d=2$), we have $(0,0)<^{\mathrm{grcolex}}(1,0)<^{\mathrm{grcolex}}(0,1)<^{\mathrm{grcolex}}(2,0)<^{\mathrm{grcolex}}(1,1)<^{\mathrm{grcolex}}(0,2)<^{\mathrm{grcolex}}(3,0)<^{\mathrm{grcolex}}(2,1)<^{\mathrm{grcolex}}(1,2)<^{\mathrm{grcolex}}(0,3)$. For $\mathcal{C}^3_3$ ($d=3$), we have $(3,0,0)<^{\mathrm{grcolex}}(2,1,0)<^{\mathrm{grcolex}}(1,2,0)<^{\mathrm{grcolex}}(0,3,0)<^{\mathrm{grcolex}}(2,0,1)<^{\mathrm{grcolex}}(1,1,1)<^{\mathrm{grcolex}}(0,2,1)<^{\mathrm{grcolex}}(1,0,2)<^{\mathrm{grcolex}}(0,1,2)<^{\mathrm{grcolex}}(0,0,3)$.

Theorems & Definitions (461)

• remark 1357
• lemma 1358: double induction by diagonal
• proof
• remark 1359
• lemma 1360: strong double induction
• proof
• remark 1361
• definition 1362: binomial coefficient
• remark 1363
• lemma 1364: properties of the binomial coefficient