1 citations · 2 across the 18 of their papers we have counts for
18 papers
Gradient descent with exponentially increasing stepsizes and restarts
François Clément, Stefan Steinerberger
Let . We consider gradient descent , where the stepsize is exponentially growing (wi…
An effective variant of the Hartigan -means algorithm
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 bette…
A Rocq Formalization of Simplicial Lagrange Finite Elements
Sylvie Boldo, François Clément, Vincent Martin +2
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 finit…
Many critical points for discrete Riesz energy on
François Clément, Stefan Steinerberger
It is widely believed that the energy functional has a number of cr…
A Rocq Formalization of Monomial and Graded Orders
Sylvie Boldo, François Clément, Vincent Martin +1
Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the fi…
Balanced Stick Breaking
François Clément, Stefan Steinerberger
Consider an infinite sequence on the unit circle . We may interpret the first elements as places where the `circular stic…
Regular Structures in Kronecker Permutations
François Clément
Kronecker sequences for some irrational have played an important role in many areas of mathematics. It is possible to associate to each finite s…
On the optimization of discrepancy measures
François Clément, Nathan Kirk, Art B. Owen +1
Numerical optimizations can find point sets with lower discrepancies than prior methods based on algebra, and discrepancies are computationally attractive for this. The …
Monotone Paths on Acyclic 3-Regular Graphs
François Clément, Dan Guyer
Motivated by trying to understand the behavior of the simplex method, Athanasiadis, De Loera and Zhang provided upper and lower bounds on the number of the monotone paths on 3-poly…
carps: A Framework for Comparing N Hyperparameter Optimizers on M Benchmarks
Carolin Benjamins, Helena Graf, Sarah Segel +14
Hyperparameter Optimization (HPO) is crucial to develop well-performing machine learning models. In order to ease prototyping and benchmarking of HPO methods, we propose carps, a b…
Small gaps in the Ulam sequence
François Clément, Stefan Steinerberger
The Ulam sequence, described by Stanislaw Ulam in the 1960s, starts and then iteratively adds the smallest integer that can be uniquely written as the sum of two distinct ear…
Failure of Orthogonality of Rounded Fourier Bases
François Clément, Stefan Steinerberger
The purpose of this note is to prove estimates for $$ \left| \sum_{k=1}^{n} \mbox{sign} \left( \cos \left( \frac{2πa}{n} k \right) \right) \mbox{sign} \left( \cos \left( \frac{2πb}…
Approximately Jumping Towards the Origin
Alex Albors, François Clément, Shosuke Kiami +3
Given an initial point and a sequence of vectors in , we define a greedy sequence by setting where…
Finite element method. Detailed proofs to be formalized in Coq
François Clément, Vincent Martin
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 mathematic…
Outperforming the Best 1D Low-Discrepancy Constructions with a Greedy Algorithm
François Clément
The design of uniformly spread sequences on has been extensively studied since the work of Weyl and van der Corput in the early century. The current best s…
Lebesgue Induction and Tonelli's Theorem in Coq
Sylvie Boldo, François Clément, Vincent Martin +2
Lebesgue integration is a well-known mathematical tool, used for instance in probability theory, real analysis, and numerical mathematics. Thus its formalization in a proof assista…
A Coq Formalization of the Bochner integral
Sylvie Boldo, François Clément, Louise Leclerc
The Bochner integral is a generalization of the Lebesgue integral, for functions taking their values in a Banach space. Therefore, both its mathematical definition and its formaliz…
Lebesgue integration. Detailed proofs to be formalized in Coq
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 result…