François Clément

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre et al.

Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre et al.

Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to guarantee their correctness. Indeed, we had to extend existing methods and tools for proving the correct behavior of programs to verify an existing numerical analysis program. This C program implements the second-order centered finite difference explicit scheme for solving the 1D wave equation. In fact, we have gone much further as we have mechanically verified the convergence of the numerical scheme in order to get a complete formal proof covering all aspects from partial differential equations to actual numerical results. To the best of our knowledge, this is the first time such a comprehensive proof is achieved.

Hend Ben Ameur, Guy Chavent, Cheikh Fatma et al.

Faults and geological barriers can drastically affect the flow patterns in porous media. Such fractures can be modeled as interfaces that interact with the surrounding matrix. We propose a new technique for the estimation of the location and hydrogeological properties of a small number of large fractures in a porous medium from given distributed pressure or flow data. At each iteration, the algorithm builds a short list of candidates by comparing fracture indicators. These indicators quantify at the first order the decrease of a data misfit function; they are cheap to compute. Then, the best candidate is picked up by minimization of the objective function for each candidate. Optimally driven by the fit to the data, the approach has the great advantage of not requiring remeshing, nor shape derivation. The stability of the algorithm is shown on a series of numerical examples representative of typical situations.

François Clément, Vincent Martin

To obtain the highest confidence on the correction of numerical simulation programs implementing the finite element method, one has to formalize the mathematical notions and results that allow to establish the soundness of the method. The Lax-Milgram theorem may be seen as one of those theoretical cornerstones: under some completeness and coercivity assumptions, it states existence and uniqueness of the solution to the weak formulation of some boundary value problems. The purpose of this document is to provide the formal proof community with a very detailed pen-and-paper proof of the Lax-Milgram theorem.

Sylvie Boldo, François Clément, Vincent Martin et al.

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.

Deyao Chen, François Clément, Carola Doerr et al.

Kernel discrepancies are a powerful tool for analyzing worst-case errors in quasi-Monte Carlo (QMC) methods. Building on recent advances in optimizing such discrepancy measures, we extend the subset selection problem to the setting of kernel discrepancies, selecting an m-element subset from a large population of size $n \gg m$. We introduce a novel subset selection algorithm applicable to general kernel discrepancies to efficiently generate low-discrepancy samples from both the uniform distribution on the unit hypercube, the traditional setting of classical QMC, and from more general distributions $F$ with known density functions by employing the kernel Stein discrepancy. We also explore the relationship between the classical $L_2$ star discrepancy and its $L_\infty$ counterpart.

François Clément, Stefan Steinerberger

The k-means problem is perhaps the classical clustering problem and often synonymous with Lloyd's algorithm (1957). It has become clear that Hartigan's algorithm (1975) gives better results in almost all cases, Telgarsky-Vattani note a typical improvement of $5\%$ -- $10\%$. We point out that a very minor variation of Hartigan's method leads to another $2\%$ -- $5\%$ improvement; the improvement tends to become larger when either dimension or $k$ increase.

Sylvie Boldo, François Clément, Jean-Christophe Filliâtre et al.

Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.

Hend Ben Ameur, François Clément, Pierre Weis et al.

The estimation of distributed parameters in partial differential equations (PDE) from measures of the solution of the PDE may lead to under-determination problems. The choice of a parameterization is a usual way of adding a-priori information by reducing the number of unknowns according to the physics of the problem. The refinement indicators algorithm provides a fruitful adaptive parameterization technique that parsimoniously opens the degrees of freedom in an iterative way. We present a new general form of the refinement indicators algorithm that is applicable to the estimation of multi-dimensional parameters in any PDE. In the linear case, we state the relationship between the refinement indicator and the decrease of the usual least-squares data misfit objective function. We give numerical results in the simple case of the identity model, and this application reveals the refinement indicators algorithm as an image segmentation technique.