A Rocq Formalization of Simplicial Lagrange Finite Elements

TL;DR

This paper formalizes the concept of finite elements within the Rocq proof assistant, focusing on simplicial Lagrange finite elements and their unisolvence proofs across dimensions and polynomial degrees.

Contribution

It provides a formal definition and proof of unisolvence for simplicial Lagrange finite elements in Rocq, covering various dimensions and polynomial degrees.

Findings

Formal definition of finite elements in Rocq

Proof of unisolvence for simplicial Lagrange finite elements

Applicable to any dimension and polynomial degree

Abstract

Formalization of mathematics is a major topic, that includes in particular numerical analysis, towards proofs of scientific computing programs. The present study is about the finite element method, a popular method to numerically solve partial differential equations. In the long-term goal of proving its correctness, we focus here on the formal definition of what is a finite element. Mathematically, a finite element describes what happens in a cell of a mesh. It notably includes the geometry of the cell, the polynomial approximation space, and a finite set of linear forms that computationally characterizes the polynomials. Formally, we design a finite element as a record in the Rocq proof assistant with both values (such as the vertices of the cell) and proofs of validity (such as the dimension of the approximation space). The decisive validity proof is unisolvence, that makes the previous characterization unique. We then instantiate this record with the most popular and useful, the simplicial Lagrange finite elements for evenly distributed nodes, for any dimension and any polynomial degree, including the difficult unisolvence proof. These proofs require many results (definitions, lemmas, canonical structures) about finite families, affine spaces, multivariate polynomials, in the context of finite or infinite-dimensional spaces.