SU\G(𝔸)/K·U
Sign Up for free Log In

Author Description

Login to generate an author description

Ask a Question About This Mathematician

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program

2012-08-13
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

Trusting computations: A mechanized proof from partial differential equations to actual program

2014-06-20
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

2021-11-23
Sylvie Boldo , François Clément , Florian Faissole +2 more
View PDF Chat

Star discrepancy subset selection: Problem formulation and efficient approaches for low dimensions

2022-01-11
François Clément , Carola Doerr , Luís Paquete
Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star … Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star discrepancy. First, we show that this problem is NP-hard. Then, we introduce a mixed integer linear formulation (MILP) and a combinatorial branch-and-bound (BB) algorithm for the star discrepancy subset selection problem and we evaluate both approaches against random subset selection and a greedy construction on different use-cases in dimension two and three. Our results show that the MILP and BB are efficient in dimension two for large and small m/n ratio, respectively, and for not too large n. However, the performance of both approaches decays strongly for larger dimensions and set sizes. As a side effect of our empirical comparisons we obtain point sets of discrepancy values that are much smaller than those of common low-discrepancy sequences, random point sets, and of Latin Hypercube Sampling. This suggests that subset selection could be an interesting approach for generating point sets of small discrepancy value.
View PDF Chat

The Lax-Milgram Theorem. A detailed proof to be formalized in Coq

2016-01-01
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 … 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.
View PDF Chat

Heuristic approaches to obtain low-discrepancy point sets via subset selection

2024-03-16
François Clément , Carola Doerr , Luís Paquete
Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the … Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the current-best subset by replacing one of its elements at a time. While the heuristic does not necessarily return an optimal solution, we obtain very promising results for all tested dimensions. For example, for moderate sizes 30≤n≤240, we obtain point sets in dimension 6 with L∞ star discrepancy up to 35% better than that of the first n points of the Sobol' sequence. Our heuristic works in all dimensions, the main limitation being the precision of the discrepancy calculation algorithms. We provide a comparison with a recent energy functional introduced by Steinerberger [J. Complexity, 2019], showing that our heuristic performs better on all tested instances. Finally, our results and complementary experiments also give further empirical information on inverse star discrepancy conjectures.
View PDF Chat

Lebesgue integration. Detailed proofs to be formalized in Coq

2021-01-01
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 … 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. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These functional spaces are built on integration and measure theory. Hence, this chapter in functional analysis is a mandatory theoretical cornerstone for the definition of the finite element method. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs of the main results from integration and measure theory.
View PDF Chat

Computing Star Discrepancies with Numerical Black-Box Optimization Algorithms

2023-07-12
François Clément , Diederick Vermetten , Jacob de Nobel +3 more
The $L_{\infty}$ star discrepancy is a measure for the regularity of a finite set of points taken from $[0,1)^d$. Low discrepancy point sets are highly relevant for Quasi-Monte Carlo methods … The $L_{\infty}$ star discrepancy is a measure for the regularity of a finite set of points taken from $[0,1)^d$. Low discrepancy point sets are highly relevant for Quasi-Monte Carlo methods in numerical integration and several other applications. Unfortunately, computing the $L_{\infty}$ star discrepancy of a given point set is known to be a hard problem, with the best exact algorithms falling short for even moderate dimensions around 8. However, despite the difficulty of finding the global maximum that defines the $L_{\infty}$ star discrepancy of the set, local evaluations at selected points are inexpensive. This makes the problem tractable by black-box optimization approaches. In this work we compare 8 popular numerical black-box optimization algorithms on the $L_{\infty}$ star discrepancy computation problem, using a wide set of instances in dimensions 2 to 15. We show that all used optimizers perform very badly on a large majority of the instances and that in many cases random search outperforms even the more sophisticated solvers. We suspect that state-of-the-art numerical black-box optimization techniques fail to capture the global structure of the problem, an important shortcoming that may guide their future development. We also provide a parallel implementation of the best-known algorithm to compute the discrepancy.
View PDF Chat

A Coq Formalization of the Bochner integral

2022-01-07
Sylvie Boldo , François Clément , Louise Leclerc
View PDF Chat

Partitions for stratified sampling

2024-01-10
François Clément , Nathan Kirk , Florian Pausinger
Abstract Classical jittered sampling partitions <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mrow> <m:mo stretchy="false">[</m:mo> <m:mn>0</m:mn> <m:mo>,</m:mo> <m:mn>1</m:mn> <m:mo stretchy="false">]</m:mo> </m:mrow> <m:mi>d</m:mi> </m:msup> </m:math> {[0,1]^{d}} into <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mi>m</m:mi> <m:mi>d</m:mi> </m:msup> </m:math> {m^{d}} … Abstract Classical jittered sampling partitions <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mrow> <m:mo stretchy="false">[</m:mo> <m:mn>0</m:mn> <m:mo>,</m:mo> <m:mn>1</m:mn> <m:mo stretchy="false">]</m:mo> </m:mrow> <m:mi>d</m:mi> </m:msup> </m:math> {[0,1]^{d}} into <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mi>m</m:mi> <m:mi>d</m:mi> </m:msup> </m:math> {m^{d}} cubes for a positive integer m and randomly places a point inside each of them, providing a point set of size <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mi>N</m:mi> <m:mo>=</m:mo> <m:msup> <m:mi>m</m:mi> <m:mi>d</m:mi> </m:msup> </m:mrow> </m:math> {N=m^{d}} with small discrepancy. The aim of this note is to provide a construction of partitions that works for arbitrary N and improves straight-forward constructions. We show how to construct equivolume partitions of the d -dimensional unit cube with hyperplanes that are orthogonal to the main diagonal of the cube. We investigate the discrepancy of such point sets and optimise the expected discrepancy numerically by relaxing the equivolume constraint using different black-box optimisation techniques.
View PDF Chat

Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program

2012-12-29
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
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 … 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.

Distribution of Distances in Five Dimensions and Related Problems

2022-09-01
François Clément , Thang Pham
In this paper, we study the Erdös--Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then … In this paper, we study the Erdös--Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then $\Delta(A^5)=\mathbb{F}_p$. When $|A-A|\sim |A|$, we are able to obtain stronger conclusions as follows: łinebreak 1. If $p^{13/22}\ll |A|\ll p^{\frac{2}{3}}$, then $(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p$. 2. If $p^{4/7}\ll |A|\ll p^{\frac{2}{3}}$, then $(A-A)^2+(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p$. We also prove that if $p^{4/7}\ll |A-A|=K|A|\le p^{5/8}$, then $|A^2+A^2|\gg \min \{ \frac{p}{K^4}, \frac{|A|^{8/3}}{K^{7/3}p^{2/3}}\}$. As a consequence, $|A^2+A^2|\gg p$ when $|A|\sim p^{5/8}$ and $K\sim 1$, where $A^2=\{x^2: x\in A\}$.
View PDF Chat

Lebesgue Induction and Tonelli's Theorem in Coq

2022-01-01
Sylvie Boldo , François Clément , Vincent Martin +2 more
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 assistant is to be designed to … 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 assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $\sigma$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.
View PDF Chat

A Coq Formalization of the Bochner integral

2022-01-01
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 formalization in the Coq … 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 formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions.
View PDF Chat

A Coq Formalization of the Bochner integral

2022-01-01
Sylvie Boldo , François Clément , Louise Leclerc
View PDF Chat

Distribution of distances in five dimensions and related problems

2021-01-01
François Clément , Thang V. Pham
In this paper, we study the Erd\H{o}s-Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then … In this paper, we study the Erd\H{o}s-Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then $\Delta(A^5)=\mathbb{F}_p$. When $|A-A|\sim |A|$, we obtain stronger statements as follows: If $|A|\gg p^{\frac{13}{22}}$, then $(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$ If $|A|\gg p^{\frac{4}{7}}$, then $(A-A)^2+(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$ We also prove that if $p^{4/7}\ll |A-A|=K|A|\le p^{5/8}$, then \[|A^2+A^2|\gg \min \left\lbrace \frac{p}{K^4}, \frac{|A|^{8/3}}{K^{7/3}p^{2/3}}\right\rbrace.\] As a consequence, $|A^2+A^2|\gg p$ when $|A|\gg p^{5/8}$ and $K\sim 1$, where $A^2=\{x^2\colon x\in A\}$.
View PDF Chat

ON THE TWO-PARAMETER ERDŐS–FALCONER DISTANCE PROBLEM IN FINITE FIELDS

2022-09-29
François Clément , Hossein Nassajian Mojarrad , Duc Hiep Pham +1 more
Abstract Given $E \subseteq \mathbb {F}_q^d \times \mathbb {F}_q^d$ , with the finite field $\mathbb {F}_q$ of order q and the integer $d\,\ge \, 2$ , we define the two-parameter … Abstract Given $E \subseteq \mathbb {F}_q^d \times \mathbb {F}_q^d$ , with the finite field $\mathbb {F}_q$ of order q and the integer $d\,\ge \, 2$ , we define the two-parameter distance set $\Delta _{d, d}(E)=\{(\|x-y\|, \|z-t\|) : (x, z), (y, t) \in E \}$ . Birklbauer and Iosevich [‘A two-parameter finite field Erdős–Falconer distance problem’, Bull. Hellenic Math. Soc. 61 (2017), 21–30] proved that if $|E| \gg q^{{(3d+1)}/{2}}$ , then $ |\Delta _{d, d}(E)| = q^2$ . For $d=2$ , they showed that if $|E| \gg q^{{10}/{3}}$ , then $ |\Delta _{2, 2}(E)| \gg q^2$ . In this paper, we give extensions and improvements of these results. Given the diagonal polynomial $P(x)=\sum _{i=1}^da_ix_i^s\in \mathbb F_q[x_1,\ldots , x_d]$ , the distance induced by P over $\mathbb {F}_q^d$ is $\|x-y\|_s:=P(x-y)$ , with the corresponding distance set $\Delta ^s_{d, d}(E)=\{(\|x-y\|_s, \|z-t\|_s) : (x, z), (y, t) \in E \}$ . We show that if $|E| \gg q^{{(3d+1)}/{2}}$ , then $ |\Delta _{d, d}^s(E)| \gg q^2$ . For $d=2$ and the Euclidean distance, we improve the former result over prime fields by showing that $ |\Delta _{2,2}(E)| \gg p^2$ for $|E| \gg p^{{13}/{4}}$ .

First-Order Indicators for the Estimation of Discrete Fractures in Porous Media

2016-01-01
Hend Ben Ameur , Guy Chavent , Cheikh Fatma +3 more
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 … 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.
View PDF Chat

Formal Proof of a Wave Equation Resolution Scheme: the Method Error

2010-01-01
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
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 … 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.
View PDF Chat

Heuristic Approaches to Obtain Low-Discrepancy Point Sets via Subset Selection

2023-01-01
François Clément , Carola Doerr , Luís Paquete
Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the … Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the current-best subset by replacing one of its elements at a time. While we prove that the heuristic does not necessarily return an optimal solution, we obtain very promising results for all tested dimensions. For example, for moderate point set sizes $30 \leq n \leq 240$ in dimension 6, we obtain point sets with $L_{\infty}$ star discrepancy up to 35% better than that of the first $n$ points of the Sobol' sequence. Our heuristic works in all dimensions, the main limitation being the precision of the discrepancy calculation algorithms. We also provide a comparison with a recent energy functional introduced by Steinerberger [J. Complexity, 2019], showing that our heuristic performs better on all tested instances.
View PDF Chat

Constructing Optimal $L_{\infty}$ Star Discrepancy Sets

2023-01-01
François Clément , Carola Doerr , Kathrin Klamroth +1 more
The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a … The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a very hard problem in the discrepancy community. Indeed, optimal point sets are, up to now, known only for $n\leq 6$ in dimension 2 and $n \leq 2$ for higher dimensions. We introduce in this paper mathematical programming formulations to construct point sets with as low $L_{\infty}$ star discrepancy as possible. Firstly, we present two models to construct optimal sets and show that there always exist optimal sets with the property that no two points share a coordinate. Then, we provide possible extensions of our models to other measures, such as the extreme and periodic discrepancies. For the $L_{\infty}$ star discrepancy, we are able to compute optimal point sets for up to 21 points in dimension 2 and for up to 8 points in dimension 3. For $d=2$ and $n\ge 7$ points, these point sets have around a 50% lower discrepancy than the current best point sets, and show a very different structure.

On the two-parameter Erdős-Falconer distance problem over finite fields

2021-01-01
François Clément , Hossein Nassajian Mojarrad , Duc Hiep Pham +1 more
Given $E \subseteq \mathbb{F}_q^d \times \mathbb{F}_q^d$, with the finite field $\mathbb{F}_q$ of order $q$ and the integer $d \ge 2$, we define the two-parameter distance set as $Δ_{d, d}(E)=\left\{\left(\|x_1-y_1\|, \|x_2-y_2\|\right) … Given $E \subseteq \mathbb{F}_q^d \times \mathbb{F}_q^d$, with the finite field $\mathbb{F}_q$ of order $q$ and the integer $d \ge 2$, we define the two-parameter distance set as $Δ_{d, d}(E)=\left\{\left(\|x_1-y_1\|, \|x_2-y_2\|\right) : (x_1,x_2), (y_1,y_2) \in E \right\}$. Birklbauer and Iosevich (2017) proved that if $|E| \gg q^{\frac{3d+1}{2}}$, then $ |Δ_{d, d}(E)| = q^2$. For the case of $d=2$, they showed that if $|E| \gg q^{\frac{10}{3}}$, then $ |Δ_{2, 2}(E)| \gg q^2$. In this paper, we present extensions and improvements of these results.

Teaching Divisibility and Binomials with Coq

2025-05-07
Sylvie Boldo , François Clément , David Hamelin +2 more
The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are … The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices and the numerous exercises we developed. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.
View PDF Chat

An Optimization Perspective on the Construction of Low-Discrepancy Point Sets

2024-07-18
François Clément
View PDF Chat

Finite element method. Detailed proofs to be formalized in Coq

2024-10-02
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 mathematical notions and results that … 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.
View PDF Chat

Transforming the Challenge of Constructing Low-Discrepancy Point Sets into a Permutation Selection Problem

2024-07-16
François Clément , Carola Doerr , Kathrin Klamroth +1 more
Low discrepancy point sets have been widely used as a tool to approximate continuous objects by discrete ones in numerical processes, for example in numerical integration. Following a century of … Low discrepancy point sets have been widely used as a tool to approximate continuous objects by discrete ones in numerical processes, for example in numerical integration. Following a century of research on the topic, it is still unclear how low the discrepancy of point sets can go; in other words, how regularly distributed can points be in a given space. Recent insights using optimization and machine learning techniques have led to substantial improvements in the construction of low-discrepancy point sets, resulting in configurations of much lower discrepancy values than previously known. Building on the optimal constructions, we present a simple way to obtain $L_{\infty}$-optimized placement of points that follow the same relative order as an (arbitrary) input set. Applying this approach to point sets in dimensions 2 and 3 for up to 400 and 50 points, respectively, we obtain point sets whose $L_{\infty}$ star discrepancies are up to 25% smaller than those of the current-best sets, and around 50% better than classical constructions such as the Fibonacci set.
View PDF Chat

Searching permutations for constructing uniformly distributed point sets

2025-04-03
François Clément , Carola Doerr , Kathrin Klamroth +1 more
Uniformly distributed point sets of low discrepancy are heavily used in experimental design and across a very wide range of applications such as numerical integration, computer graphics, and finance. Recent … Uniformly distributed point sets of low discrepancy are heavily used in experimental design and across a very wide range of applications such as numerical integration, computer graphics, and finance. Recent methods based on Graph Neural Networks [T. K. Rusch, N. Kirk, M. M. Bronstein, C. Lemieux, D. Rus, Proc. Natl. Acad. Sci. U.S.A. 121, e2409913121 (2024).] and solver-based optimization identified point sets having much lower discrepancy than previously known constructions. We show in this note that further substantial improvements are possible by separating the construction of low-discrepancy point sets into i) the relative position of the points, and ii) the optimal placement respecting these relationships. Using tailored permutations, we construct point sets that are of 20% smaller discrepancy on average than those proposed by Rusch et al. In terms of inverse discrepancy, our sets reduce the number of points in dimension 2 needed to obtain a discrepancy of 0.005 from more than 500 points to less than 350. For applications where the sets are used to query time-consuming models, this is a significant reduction.

Constructing optimal star discrepancy sets

2025-05-02
François Clément , Carola Doerr , Kathrin Klamroth +1 more
We provide in this paper a constructive proof of optimal <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper L Subscript normal infinity"> <mml:semantics> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="normal">∞</mml:mi> </mml:mrow> </mml:msub> <mml:annotation encoding="application/x-tex">L_{\infty … We provide in this paper a constructive proof of optimal <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper L Subscript normal infinity"> <mml:semantics> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="normal">∞</mml:mi> </mml:mrow> </mml:msub> <mml:annotation encoding="application/x-tex">L_{\infty }</mml:annotation> </mml:semantics> </mml:math> </inline-formula> star discrepancy values in dimension 2 for up to 21 points and up to 8 points in dimension 3. This extends work by White (Numer. Math. <bold>27</bold> (1976/77), no. 2, 157–164) for up to six points in dimension 2 and of Larcher and Pillichshammer (J. Comput. Appl. Math. <bold>206</bold> (2007), no. 2, 977–985) for two points in arbitrary dimensions. We show that these optimal sets have a far lower discrepancy than the previous references and, perhaps more importantly, present a very different structure.

Teaching Divisibility and Binomials with Coq

2025-05-07
Sylvie Boldo , François Clément , David Hamelin +2 more
The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are … The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices and the numerous exercises we developed. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.
View PDF Chat

Constructing optimal star discrepancy sets

2025-05-02
François Clément , Carola Doerr , Kathrin Klamroth +1 more
We provide in this paper a constructive proof of optimal <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper L Subscript normal infinity"> <mml:semantics> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="normal">∞</mml:mi> </mml:mrow> </mml:msub> <mml:annotation encoding="application/x-tex">L_{\infty … We provide in this paper a constructive proof of optimal <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper L Subscript normal infinity"> <mml:semantics> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="normal">∞</mml:mi> </mml:mrow> </mml:msub> <mml:annotation encoding="application/x-tex">L_{\infty }</mml:annotation> </mml:semantics> </mml:math> </inline-formula> star discrepancy values in dimension 2 for up to 21 points and up to 8 points in dimension 3. This extends work by White (Numer. Math. <bold>27</bold> (1976/77), no. 2, 157–164) for up to six points in dimension 2 and of Larcher and Pillichshammer (J. Comput. Appl. Math. <bold>206</bold> (2007), no. 2, 977–985) for two points in arbitrary dimensions. We show that these optimal sets have a far lower discrepancy than the previous references and, perhaps more importantly, present a very different structure.

Searching permutations for constructing uniformly distributed point sets

2025-04-03
François Clément , Carola Doerr , Kathrin Klamroth +1 more
Uniformly distributed point sets of low discrepancy are heavily used in experimental design and across a very wide range of applications such as numerical integration, computer graphics, and finance. Recent … Uniformly distributed point sets of low discrepancy are heavily used in experimental design and across a very wide range of applications such as numerical integration, computer graphics, and finance. Recent methods based on Graph Neural Networks [T. K. Rusch, N. Kirk, M. M. Bronstein, C. Lemieux, D. Rus, Proc. Natl. Acad. Sci. U.S.A. 121, e2409913121 (2024).] and solver-based optimization identified point sets having much lower discrepancy than previously known constructions. We show in this note that further substantial improvements are possible by separating the construction of low-discrepancy point sets into i) the relative position of the points, and ii) the optimal placement respecting these relationships. Using tailored permutations, we construct point sets that are of 20% smaller discrepancy on average than those proposed by Rusch et al. In terms of inverse discrepancy, our sets reduce the number of points in dimension 2 needed to obtain a discrepancy of 0.005 from more than 500 points to less than 350. For applications where the sets are used to query time-consuming models, this is a significant reduction.

Finite element method. Detailed proofs to be formalized in Coq

2024-10-02
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 mathematical notions and results that … 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.
View PDF Chat

An Optimization Perspective on the Construction of Low-Discrepancy Point Sets

2024-07-18
François Clément
View PDF Chat

Transforming the Challenge of Constructing Low-Discrepancy Point Sets into a Permutation Selection Problem

2024-07-16
François Clément , Carola Doerr , Kathrin Klamroth +1 more
Low discrepancy point sets have been widely used as a tool to approximate continuous objects by discrete ones in numerical processes, for example in numerical integration. Following a century of … Low discrepancy point sets have been widely used as a tool to approximate continuous objects by discrete ones in numerical processes, for example in numerical integration. Following a century of research on the topic, it is still unclear how low the discrepancy of point sets can go; in other words, how regularly distributed can points be in a given space. Recent insights using optimization and machine learning techniques have led to substantial improvements in the construction of low-discrepancy point sets, resulting in configurations of much lower discrepancy values than previously known. Building on the optimal constructions, we present a simple way to obtain $L_{\infty}$-optimized placement of points that follow the same relative order as an (arbitrary) input set. Applying this approach to point sets in dimensions 2 and 3 for up to 400 and 50 points, respectively, we obtain point sets whose $L_{\infty}$ star discrepancies are up to 25% smaller than those of the current-best sets, and around 50% better than classical constructions such as the Fibonacci set.
View PDF Chat

Heuristic approaches to obtain low-discrepancy point sets via subset selection

2024-03-16
François Clément , Carola Doerr , Luís Paquete
Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the … Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the current-best subset by replacing one of its elements at a time. While the heuristic does not necessarily return an optimal solution, we obtain very promising results for all tested dimensions. For example, for moderate sizes 30≤n≤240, we obtain point sets in dimension 6 with L∞ star discrepancy up to 35% better than that of the first n points of the Sobol' sequence. Our heuristic works in all dimensions, the main limitation being the precision of the discrepancy calculation algorithms. We provide a comparison with a recent energy functional introduced by Steinerberger [J. Complexity, 2019], showing that our heuristic performs better on all tested instances. Finally, our results and complementary experiments also give further empirical information on inverse star discrepancy conjectures.
View PDF Chat

Partitions for stratified sampling

2024-01-10
François Clément , Nathan Kirk , Florian Pausinger
Abstract Classical jittered sampling partitions <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mrow> <m:mo stretchy="false">[</m:mo> <m:mn>0</m:mn> <m:mo>,</m:mo> <m:mn>1</m:mn> <m:mo stretchy="false">]</m:mo> </m:mrow> <m:mi>d</m:mi> </m:msup> </m:math> {[0,1]^{d}} into <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mi>m</m:mi> <m:mi>d</m:mi> </m:msup> </m:math> {m^{d}} … Abstract Classical jittered sampling partitions <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mrow> <m:mo stretchy="false">[</m:mo> <m:mn>0</m:mn> <m:mo>,</m:mo> <m:mn>1</m:mn> <m:mo stretchy="false">]</m:mo> </m:mrow> <m:mi>d</m:mi> </m:msup> </m:math> {[0,1]^{d}} into <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:msup> <m:mi>m</m:mi> <m:mi>d</m:mi> </m:msup> </m:math> {m^{d}} cubes for a positive integer m and randomly places a point inside each of them, providing a point set of size <m:math xmlns:m="http://www.w3.org/1998/Math/MathML"> <m:mrow> <m:mi>N</m:mi> <m:mo>=</m:mo> <m:msup> <m:mi>m</m:mi> <m:mi>d</m:mi> </m:msup> </m:mrow> </m:math> {N=m^{d}} with small discrepancy. The aim of this note is to provide a construction of partitions that works for arbitrary N and improves straight-forward constructions. We show how to construct equivolume partitions of the d -dimensional unit cube with hyperplanes that are orthogonal to the main diagonal of the cube. We investigate the discrepancy of such point sets and optimise the expected discrepancy numerically by relaxing the equivolume constraint using different black-box optimisation techniques.
View PDF Chat

Computing Star Discrepancies with Numerical Black-Box Optimization Algorithms

2023-07-12
François Clément , Diederick Vermetten , Jacob de Nobel +3 more
The $L_{\infty}$ star discrepancy is a measure for the regularity of a finite set of points taken from $[0,1)^d$. Low discrepancy point sets are highly relevant for Quasi-Monte Carlo methods … The $L_{\infty}$ star discrepancy is a measure for the regularity of a finite set of points taken from $[0,1)^d$. Low discrepancy point sets are highly relevant for Quasi-Monte Carlo methods in numerical integration and several other applications. Unfortunately, computing the $L_{\infty}$ star discrepancy of a given point set is known to be a hard problem, with the best exact algorithms falling short for even moderate dimensions around 8. However, despite the difficulty of finding the global maximum that defines the $L_{\infty}$ star discrepancy of the set, local evaluations at selected points are inexpensive. This makes the problem tractable by black-box optimization approaches. In this work we compare 8 popular numerical black-box optimization algorithms on the $L_{\infty}$ star discrepancy computation problem, using a wide set of instances in dimensions 2 to 15. We show that all used optimizers perform very badly on a large majority of the instances and that in many cases random search outperforms even the more sophisticated solvers. We suspect that state-of-the-art numerical black-box optimization techniques fail to capture the global structure of the problem, an important shortcoming that may guide their future development. We also provide a parallel implementation of the best-known algorithm to compute the discrepancy.
View PDF Chat

Heuristic Approaches to Obtain Low-Discrepancy Point Sets via Subset Selection

2023-01-01
François Clément , Carola Doerr , Luís Paquete
Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the … Building upon the exact methods presented in our earlier work [J. Complexity, 2022], we introduce a heuristic approach for the star discrepancy subset selection problem. The heuristic gradually improves the current-best subset by replacing one of its elements at a time. While we prove that the heuristic does not necessarily return an optimal solution, we obtain very promising results for all tested dimensions. For example, for moderate point set sizes $30 \leq n \leq 240$ in dimension 6, we obtain point sets with $L_{\infty}$ star discrepancy up to 35% better than that of the first $n$ points of the Sobol' sequence. Our heuristic works in all dimensions, the main limitation being the precision of the discrepancy calculation algorithms. We also provide a comparison with a recent energy functional introduced by Steinerberger [J. Complexity, 2019], showing that our heuristic performs better on all tested instances.
View PDF Chat

Constructing Optimal $L_{\infty}$ Star Discrepancy Sets

2023-01-01
François Clément , Carola Doerr , Kathrin Klamroth +1 more
The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a … The $L_{\infty}$ star discrepancy is a very well-studied measure used to quantify the uniformity of a point set distribution. Constructing optimal point sets for this measure is seen as a very hard problem in the discrepancy community. Indeed, optimal point sets are, up to now, known only for $n\leq 6$ in dimension 2 and $n \leq 2$ for higher dimensions. We introduce in this paper mathematical programming formulations to construct point sets with as low $L_{\infty}$ star discrepancy as possible. Firstly, we present two models to construct optimal sets and show that there always exist optimal sets with the property that no two points share a coordinate. Then, we provide possible extensions of our models to other measures, such as the extreme and periodic discrepancies. For the $L_{\infty}$ star discrepancy, we are able to compute optimal point sets for up to 21 points in dimension 2 and for up to 8 points in dimension 3. For $d=2$ and $n\ge 7$ points, these point sets have around a 50% lower discrepancy than the current best point sets, and show a very different structure.

ON THE TWO-PARAMETER ERDŐS–FALCONER DISTANCE PROBLEM IN FINITE FIELDS

2022-09-29
François Clément , Hossein Nassajian Mojarrad , Duc Hiep Pham +1 more
Abstract Given $E \subseteq \mathbb {F}_q^d \times \mathbb {F}_q^d$ , with the finite field $\mathbb {F}_q$ of order q and the integer $d\,\ge \, 2$ , we define the two-parameter … Abstract Given $E \subseteq \mathbb {F}_q^d \times \mathbb {F}_q^d$ , with the finite field $\mathbb {F}_q$ of order q and the integer $d\,\ge \, 2$ , we define the two-parameter distance set $\Delta _{d, d}(E)=\{(\|x-y\|, \|z-t\|) : (x, z), (y, t) \in E \}$ . Birklbauer and Iosevich [‘A two-parameter finite field Erdős–Falconer distance problem’, Bull. Hellenic Math. Soc. 61 (2017), 21–30] proved that if $|E| \gg q^{{(3d+1)}/{2}}$ , then $ |\Delta _{d, d}(E)| = q^2$ . For $d=2$ , they showed that if $|E| \gg q^{{10}/{3}}$ , then $ |\Delta _{2, 2}(E)| \gg q^2$ . In this paper, we give extensions and improvements of these results. Given the diagonal polynomial $P(x)=\sum _{i=1}^da_ix_i^s\in \mathbb F_q[x_1,\ldots , x_d]$ , the distance induced by P over $\mathbb {F}_q^d$ is $\|x-y\|_s:=P(x-y)$ , with the corresponding distance set $\Delta ^s_{d, d}(E)=\{(\|x-y\|_s, \|z-t\|_s) : (x, z), (y, t) \in E \}$ . We show that if $|E| \gg q^{{(3d+1)}/{2}}$ , then $ |\Delta _{d, d}^s(E)| \gg q^2$ . For $d=2$ and the Euclidean distance, we improve the former result over prime fields by showing that $ |\Delta _{2,2}(E)| \gg p^2$ for $|E| \gg p^{{13}/{4}}$ .

Distribution of Distances in Five Dimensions and Related Problems

2022-09-01
François Clément , Thang Pham
In this paper, we study the Erdös--Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then … In this paper, we study the Erdös--Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then $\Delta(A^5)=\mathbb{F}_p$. When $|A-A|\sim |A|$, we are able to obtain stronger conclusions as follows: łinebreak 1. If $p^{13/22}\ll |A|\ll p^{\frac{2}{3}}$, then $(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p$. 2. If $p^{4/7}\ll |A|\ll p^{\frac{2}{3}}$, then $(A-A)^2+(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p$. We also prove that if $p^{4/7}\ll |A-A|=K|A|\le p^{5/8}$, then $|A^2+A^2|\gg \min \{ \frac{p}{K^4}, \frac{|A|^{8/3}}{K^{7/3}p^{2/3}}\}$. As a consequence, $|A^2+A^2|\gg p$ when $|A|\sim p^{5/8}$ and $K\sim 1$, where $A^2=\{x^2: x\in A\}$.
View PDF Chat

Star discrepancy subset selection: Problem formulation and efficient approaches for low dimensions

2022-01-11
François Clément , Carola Doerr , Luís Paquete
Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star … Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star discrepancy. First, we show that this problem is NP-hard. Then, we introduce a mixed integer linear formulation (MILP) and a combinatorial branch-and-bound (BB) algorithm for the star discrepancy subset selection problem and we evaluate both approaches against random subset selection and a greedy construction on different use-cases in dimension two and three. Our results show that the MILP and BB are efficient in dimension two for large and small m/n ratio, respectively, and for not too large n. However, the performance of both approaches decays strongly for larger dimensions and set sizes. As a side effect of our empirical comparisons we obtain point sets of discrepancy values that are much smaller than those of common low-discrepancy sequences, random point sets, and of Latin Hypercube Sampling. This suggests that subset selection could be an interesting approach for generating point sets of small discrepancy value.
View PDF Chat

A Coq Formalization of the Bochner integral

2022-01-07
Sylvie Boldo , François Clément , Louise Leclerc
View PDF Chat

Lebesgue Induction and Tonelli's Theorem in Coq

2022-01-01
Sylvie Boldo , François Clément , Vincent Martin +2 more
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 assistant is to be designed to … 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 assistant is to be designed to fit different goals and projects. Once Lebesgue integral is formally defined and the first lemmas are proved, the question of the convenience of the formalization naturally arises. To check it, a useful extension is the Tonelli theorem, stating that the (double) integral of a nonnegative measurable function of two variables can be computed by iterated integrals, and allowing to switch the order of integration. Therefore, we need to define and prove results on product spaces, hoping that they can easily derive from the existing ones on a single space. This article describes the formal definition and proof in Coq of product $\sigma$-algebras, product measures and their uniqueness, the construction of iterated integrals, up to the Tonelli theorem. We also advertise the \emph{Lebesgue induction principle} provided by an inductive type for {\nonnegative} measurable functions.
View PDF Chat

A Coq Formalization of the Bochner integral

2022-01-01
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 formalization in the Coq … 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 formalization in the Coq proof assistant are more challenging as we cannot rely on the properties of real numbers. Our contributions include an original formalization of simple functions, Bochner integrability defined by a dependent type, and the construction of the proof of the integrability of measurable functions under mild hypotheses (weak separability). Then, we define the Bochner integral and prove several theorems, including dominated convergence and the equivalence with an existing formalization of Lebesgue integral for nonnegative functions.
View PDF Chat

A Coq Formalization of the Bochner integral

2022-01-01
Sylvie Boldo , François Clément , Louise Leclerc
View PDF Chat

A Coq Formalization of Lebesgue Integration of Nonnegative Functions

2021-11-23
Sylvie Boldo , François Clément , Florian Faissole +2 more
View PDF Chat

Lebesgue integration. Detailed proofs to be formalized in Coq

2021-01-01
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 … 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. Sobolev spaces are the mathematical framework in which most weak formulations of partial derivative equations are stated, and where solutions are sought. These functional spaces are built on integration and measure theory. Hence, this chapter in functional analysis is a mandatory theoretical cornerstone for the definition of the finite element method. The purpose of this document is to provide the formal proof community with very detailed pen-and-paper proofs of the main results from integration and measure theory.
View PDF Chat

Distribution of distances in five dimensions and related problems

2021-01-01
François Clément , Thang V. Pham
In this paper, we study the Erd\H{o}s-Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then … In this paper, we study the Erd\H{o}s-Falconer distance problem in five dimensions for sets of Cartesian product structures. More precisely, we show that for $A\subset \mathbb{F}_p$ with $|A|\gg p^{\frac{13}{22}}$, then $\Delta(A^5)=\mathbb{F}_p$. When $|A-A|\sim |A|$, we obtain stronger statements as follows: If $|A|\gg p^{\frac{13}{22}}$, then $(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$ If $|A|\gg p^{\frac{4}{7}}$, then $(A-A)^2+(A-A)^2+A^2+A^2+A^2+A^2=\mathbb{F}_p.$ We also prove that if $p^{4/7}\ll |A-A|=K|A|\le p^{5/8}$, then \[|A^2+A^2|\gg \min \left\lbrace \frac{p}{K^4}, \frac{|A|^{8/3}}{K^{7/3}p^{2/3}}\right\rbrace.\] As a consequence, $|A^2+A^2|\gg p$ when $|A|\gg p^{5/8}$ and $K\sim 1$, where $A^2=\{x^2\colon x\in A\}$.
View PDF Chat

On the two-parameter Erdős-Falconer distance problem over finite fields

2021-01-01
François Clément , Hossein Nassajian Mojarrad , Duc Hiep Pham +1 more
Given $E \subseteq \mathbb{F}_q^d \times \mathbb{F}_q^d$, with the finite field $\mathbb{F}_q$ of order $q$ and the integer $d \ge 2$, we define the two-parameter distance set as $Δ_{d, d}(E)=\left\{\left(\|x_1-y_1\|, \|x_2-y_2\|\right) … Given $E \subseteq \mathbb{F}_q^d \times \mathbb{F}_q^d$, with the finite field $\mathbb{F}_q$ of order $q$ and the integer $d \ge 2$, we define the two-parameter distance set as $Δ_{d, d}(E)=\left\{\left(\|x_1-y_1\|, \|x_2-y_2\|\right) : (x_1,x_2), (y_1,y_2) \in E \right\}$. Birklbauer and Iosevich (2017) proved that if $|E| \gg q^{\frac{3d+1}{2}}$, then $ |Δ_{d, d}(E)| = q^2$. For the case of $d=2$, they showed that if $|E| \gg q^{\frac{10}{3}}$, then $ |Δ_{2, 2}(E)| \gg q^2$. In this paper, we present extensions and improvements of these results.

The Lax-Milgram Theorem. A detailed proof to be formalized in Coq

2016-01-01
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 … 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.
View PDF Chat

First-Order Indicators for the Estimation of Discrete Fractures in Porous Media

2016-01-01
Hend Ben Ameur , Guy Chavent , Cheikh Fatma +3 more
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 … 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.
View PDF Chat

Trusting computations: A mechanized proof from partial differential equations to actual program

2014-06-20
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

Trusting Computations: a Mechanized Proof from Partial Differential Equations to Actual Program

2012-12-29
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
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 … 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.

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program

2012-08-13
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

Formal Proof of a Wave Equation Resolution Scheme: the Method Error

2010-01-01
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
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 … 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.
View PDF Chat
Coauthor Papers Together
Sylvie Boldo 10
Luís Paquete 8
Carola Doerr 8
Micaela Mayero 7
Kathrin Klamroth 4
Vincent Martin 4
Guillaume Melquiond 4
Pierre Weis 4
Jean-Christophe Filliâtre 4
Louise Leclerc 3
Vincent Martin 2
Duc Hiep Pham 2
Chun‐Yen Shen 2
Hossein Nassajian Mojarrad 2
Thang Pham 1
Jean E. Roberts 1
Thang V. Pham 1
Cheikh Fatma 1
Jacob de Nobel 1
Alexandre D. Jesus 1
Pierre Rousselin 1
Guy Chavent 1
Houda Mouhcine 1
Hend Ben Ameur 1
Nathan Kirk 1
Florian Faissole 1
Diederick Vermetten 1
Florian Pausinger 1
David Hamelin 1

Low-Discrepancy Sequences

1997-08-31
Silvio Galanti , Alan Jung
<h3></h3> It has been estimated that malnutrition affects 50% of hospice patients. Nutritional assessment and support is vital in palliative care, since inadequate hydration and nutrition results in skin and … <h3></h3> It has been estimated that malnutrition affects 50% of hospice patients. Nutritional assessment and support is vital in palliative care, since inadequate hydration and nutrition results in skin and muscle wasting, vulnerability to the development of pressure ulcers, and susceptibility to infection. <h3>Method</h3> Clinical and catering staff established a nutritional steering group with the brief of introducing an assessment tool and improving the evaluation and management of nutritional risk in the hospice. The group identified several nutritional assessment tools and concluded that none were ideal for use in the hospice setting. The Nutritional Screening Tool was adapted to identify significant risk of nutritional problems in inpatients. The group devised a new policy and procedure for nutritional care along with an information leaflet for patients and families to support them in managing their own nutritional risk. Inpatients were given the opportunity to choose meals, snacks and drinks. Training for all staff on nutritional assessment using the tool and management of nutritional risk was provided <h3>Results</h3> Following staff training and implementation of the assessment tool, an audit was undertaken which showed: 96% of patients had a nutritional assessment completed within 24 h of admission. 100% of patients requiring an individualised care plan had one formulated. 89% of all patient meals were recorded by catering team. <h3>Conclusion</h3> This simple intervention made a significant improvement in the assessment and management of nutritional risk in the hospice inpatient population compared to the baseline audit prior to the revised policy. Clinical and Catering staff working together has made a positive impact on practice for inpatients. In recognition that people admitted to the hospice are often frailer and more likely to already have established malnutrition, the nutritional tool has now been introduced to the hospice outpatient services. This will hopefully delay the onset of malnutrition in these patients.

Discrepancy and convex programming

1972-12-01
Harald Niederreiter
View PDF Chat

MatBuilder

2022-07-01
Loïs Paulin , Nicolas Bonneel , David Cœurjolly +3 more
Many applications ranging from quasi-Monte Carlo integration over optimal control to neural networks benefit from high-dimensional, highly uniform samples. In the case of computer graphics, and more particularly in rendering, … Many applications ranging from quasi-Monte Carlo integration over optimal control to neural networks benefit from high-dimensional, highly uniform samples. In the case of computer graphics, and more particularly in rendering, despite the need for uniformity, several sub-problems expose a low-dimensional structure. In this context, mastering sampling uniformity over projections while preserving high-dimensional uniformity has been intrinsically challenging. This difficulty may explain the relatively small number of mathematical constructions for such samplers. We propose a novel approach by showing that uniformity constraints can be expressed as an integer linear program that results in a sampler with the desired properties. As it turns out, complex constraints are easy to describe by means of stratification and sequence properties of digital nets. Formalized using generator matrix determinants, our new MatBuilder software solves the set of constraints by iterating the linear integer program solver in a greedy fashion to compute a problem-specific set of generator matrices that can be used as a drop-in replacement in the popular digital net samplers. The samplers created by MatBuilder achieve the uniformity of classic low discrepancy sequences. More importantly, we demonstrate the benefit of the unprecedented versatility of our constraint approach with respect to low-dimensional problem structure for several applications.
View PDF Chat

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program

2012-08-13
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

Finding optimal volume subintervals with k points and calculating the star discrepancy are NP-hard problems

2008-12-03
Michael Gnewuch , Anand Srivastav , Carola Winzen

The inverse of the star-discrepancy depends linearly on the dimension

2001-01-01
Stefan Heinrich , Henryk Woźniakowski , Grzegorz W. Wasilkowski +1 more
We study bounds on the classical ∗-discrepancy and on its inverse. Let n∞(d, e) be the inverse of the ∗-discrepancy, i.e., the minimal number of points in dimension d with … We study bounds on the classical ∗-discrepancy and on its inverse. Let n∞(d, e) be the inverse of the ∗-discrepancy, i.e., the minimal number of points in dimension d with the ∗-discrepancy at most e. We prove that n∞(d, e) depends linearly on d and at most quadratically on e−1. We present three upper bounds on n∞(d, e), all of them are based on probabilistic arguments and therefore they are non-constructive. The linear in d upper bound directly follows from deep results of the theory of empirical processes but it contains an unknown multiplicative factor. Two other upper bounds are without unknown factors but do not yield the linear (in d) upper bound. One upper bound is based on an average case analysis for the Lp-star discrepancy and our numerical results seem to indicate that it gives the best estimates for specific values of d and e. We also present two lower bounds on n∞(d, e). For lower bounds, we allow arbitrary coefficients in the discrepancy formula. We prove that n∞(d, e) must be of order d log e−1 and, roughly, of order dλe−(1−λ) for any λ ∈ (0, 1).
View PDF Chat

Hardness of discrepancy computation and <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si9.gif" display="inline" overflow="scroll"><mml:mi>ε</mml:mi></mml:math>-net verification in high dimension

2011-10-17
Panos Giannopoulos , Christian Knauer , Magnus Wahlström +1 more

On the Small Ball Inequality in all dimensions

2007-11-10
Dmitriy Bilyk , Michael T. Lacey , Armen Vagharshakyan
View PDF Chat

A New Randomized Algorithm to Approximate the Star Discrepancy Based on Threshold Accepting

2012-01-01
Michael Gnewuch , Magnus Wahlström , Carola Winzen
We present a new algorithm for estimating the star discrepancy of arbitrary point sets. Similar to the algorithm for discrepancy approximation of Winker and Fang [SIAM J. Numer. Anal. 34 … We present a new algorithm for estimating the star discrepancy of arbitrary point sets. Similar to the algorithm for discrepancy approximation of Winker and Fang [SIAM J. Numer. Anal. 34 (1997), 2028--2042] it is based on the optimization algorithm threshold accepting. Our improvements include, amongst others, a non-uniform sampling strategy which is more suited for higher-dimensional inputs, and rounding steps which transform axis-parallel boxes, on which the discrepancy is to be tested, into \emph{critical test boxes}. These critical test boxes provably yield higher discrepancy values, and contain the box that exhibits the maximum value of the local discrepancy. We provide comprehensive experiments to test the new algorithm. Our randomized algorithm computes the exact discrepancy frequently in all cases where this can be checked (i.e., where the exact discrepancy of the point set can be computed in feasible time). Most importantly, in higher dimension the new method behaves clearly better than all previously known methods.
View PDF Chat

On optimal extreme-discrepancy point sets in the square

1977-06-01
Brian E. White

Partial Differential Equations

1982-01-01
Fritz John

Fibonacci sets and symmetrization in discrepancy theory

2011-08-21
Dmitriy Bilyk , Vladimir Temlyakov , Rui Yu

Positive Sums of the Classical Orthogonal Polynomials

1977-05-01
George Gasper
An expansion as a sum of squares of Jacobi polynomials $P_n^{(\alpha ,\beta )} (x)$ is used to prove that if $0 \leqq \lambda \leqq \alpha + \beta $ and $\beta … An expansion as a sum of squares of Jacobi polynomials $P_n^{(\alpha ,\beta )} (x)$ is used to prove that if $0 \leqq \lambda \leqq \alpha + \beta $ and $\beta \geqq - {1 / 2}$, then \[( * )\qquad \sum_{k = 0}^n {\frac{{(\lambda + 1)_{n - k} }}{{(n - k)!}}} \frac{{(\lambda + 1)_k }}{{k!}}\frac{{P_k^{(\alpha ,\beta )} }}(x){{P_k^{(\beta ,\alpha )}(i) }} \geqq 0,\quad - 1 \leqq x < \infty ,\] and the only cases of equality occur when $x = - 1$ for n odd and when $\lambda = 0$, $\alpha = - \beta = {1 / 2}$. Additional conditions are given under which $( * )$ holds and some special uses, limit cases, and important applications are pointed out. In particular, the case $\lambda = \alpha + \beta $ of $( * )$ is used to prove that if $\alpha $, $\beta \geqq - {1 / 2}$ then the Cesàro $(C,\alpha + \beta + 2)$ means of the Jacobi series of a nonnegative function are nonnegative. Also, it is shown that \[\frac{d}{{d\theta }}\sum\limits_{k = 0}^n {\frac{{(\lambda + 1)_{n - k} }}{{(n - k)!}}} \frac{{(\lambda + 1)_k }}{{k!}}\frac{{\sin (k + 1)\theta }}{{(k + 1)\sin ({\theta / 2})}} < 0,\qquad 1 < \theta < \pi ,\quad 0 \leqq \lambda \leqq 1,\] which extends a recent result of Askey and Steinig.

Bracketing numbers for axis-parallel boxes and applications to geometric discrepancy

2007-10-02
Michael Gnewuch

A Panorama of Discrepancy Theory

2014-01-01
William Chen , Anand Srivastav , Giancarlo Travaglini

On the pinned distances problem in positive characteristic

2022-01-01
Thomas Brendan Murphy , Giorgis Petridis , Thang Pham +2 more
We study the Erd\H os-Falconer distance problem for a set $A\subset \mathbb{F}^2$, where $\mathbb{F}$ is a field of positive characteristic $p$. If $\mathbb{F}=\mathbb{F}_p$ and the cardinality $|A|$ exceeds $p^{5/4}$, we … We study the Erd\H os-Falconer distance problem for a set $A\subset \mathbb{F}^2$, where $\mathbb{F}$ is a field of positive characteristic $p$. If $\mathbb{F}=\mathbb{F}_p$ and the cardinality $|A|$ exceeds $p^{5/4}$, we prove that $A$ determines an asymptotically full proportion of the feasible $p$ distances. For small sets $A$, namely when $|A|\leq p^{4/3}$ over any $\mathbb{F}$, we prove that either $A$ determines $\gg|A|^{2/3}$. For both large and small sets, the results proved are in fact for pinned distances.
View PDF Chat

Calculation of Discrepancy Measures and Applications

2014-01-01
Carola Doerr , Michael Gnewuch , Magnus Wahlström
View PDF Chat

Erdös distance problem in vector spaces over finite fields

2007-07-20
Alex Iosevich , M. Rudnev
We study the Erdös/Falconer distance problem in vector spaces over finite fields. Let <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper F Subscript q"> <mml:semantics> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> … We study the Erdös/Falconer distance problem in vector spaces over finite fields. Let <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper F Subscript q"> <mml:semantics> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>q</mml:mi> </mml:msub> <mml:annotation encoding="application/x-tex">{\mathbb F}_q</mml:annotation> </mml:semantics> </mml:math> </inline-formula> be a finite field with <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="q"> <mml:semantics> <mml:mi>q</mml:mi> <mml:annotation encoding="application/x-tex">q</mml:annotation> </mml:semantics> </mml:math> </inline-formula> elements and take <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper E subset-of double-struck upper F Subscript q Superscript d"> <mml:semantics> <mml:mrow> <mml:mi>E</mml:mi> <mml:mo>⊂</mml:mo> <mml:msubsup> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>q</mml:mi> <mml:mi>d</mml:mi> </mml:msubsup> </mml:mrow> <mml:annotation encoding="application/x-tex">E \subset {\mathbb F}^d_q</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="d greater-than-or-equal-to 2"> <mml:semantics> <mml:mrow> <mml:mi>d</mml:mi> <mml:mo>≥</mml:mo> <mml:mn>2</mml:mn> </mml:mrow> <mml:annotation encoding="application/x-tex">d \ge 2</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. We develop a Fourier analytic machinery, analogous to that developed by Mattila in the continuous case, for the study of distance sets in <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper F Subscript q Superscript d"> <mml:semantics> <mml:msubsup> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>q</mml:mi> <mml:mi>d</mml:mi> </mml:msubsup> <mml:annotation encoding="application/x-tex">{\mathbb F}^d_q</mml:annotation> </mml:semantics> </mml:math> </inline-formula> to provide estimates for minimum cardinality of the distance set <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Delta left-parenthesis upper E right-parenthesis"> <mml:semantics> <mml:mrow> <mml:mi mathvariant="normal">Δ</mml:mi> <mml:mo stretchy="false">(</mml:mo> <mml:mi>E</mml:mi> <mml:mo stretchy="false">)</mml:mo> </mml:mrow> <mml:annotation encoding="application/x-tex">\Delta (E)</mml:annotation> </mml:semantics> </mml:math> </inline-formula> in terms of the cardinality of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper E"> <mml:semantics> <mml:mi>E</mml:mi> <mml:annotation encoding="application/x-tex">E</mml:annotation> </mml:semantics> </mml:math> </inline-formula>. Bounds for Gauss and Kloosterman sums play an important role in the proof.
View PDF Chat

Formal Proof of a Wave Equation Resolution Scheme: The Method Error

2010-01-01
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

Distribution of distances in positive characteristic

2020-12-31
Thang Pham , Lê Anh Vinh
Let $\mathbb{F}_q$ be an arbitrary finite field, and $\mathcal{E}$ be a set of points in $\mathbb{F}_q^d$. Let $\Delta(\mathcal{E})$ be the set of distances determined by pairs of points in $\mathcal{E}$. … Let $\mathbb{F}_q$ be an arbitrary finite field, and $\mathcal{E}$ be a set of points in $\mathbb{F}_q^d$. Let $\Delta(\mathcal{E})$ be the set of distances determined by pairs of points in $\mathcal{E}$. By using the Kloosterman sums, Iosevich and Rudnev proved that if $|\mathcal{E}|\ge 4q^{\frac{d+1}{2}}$, then $\Delta(\mathcal{E})=\mathbb{F}_q$. In general, this result is sharp in odd-dimensional spaces over arbitrary finite fields. In this paper, we use the recent point-plane incidence bound due to Rudnev to prove that if $\mathcal{E}$ has Cartesian product structure in vector spaces over prime fields, then we can break the exponent $(d+1)/2$, and still cover all distances. We also show that the number of pairs of points in $\mathcal{E}$ of any given distance is close to its expected value.
View PDF Chat

Black-Box Optimization Revisited: Improving Algorithm Selection Wizards Through Massive Benchmarking

2021-08-27
Laurent Meunier , Herilalaina Rakotoarison , Pak Kan Wong +5 more
Existing studies in black-box optimization suffer from low generalizability, caused by a typically selective choice of problem instances used for training and testing of different optimization algorithms. Among other issues, … Existing studies in black-box optimization suffer from low generalizability, caused by a typically selective choice of problem instances used for training and testing of different optimization algorithms. Among other issues, this practice promotes overfitting and poor-performing user guidelines. We address this shortcoming by introducing in this work a general-purpose algorithm selection wizard that was designed and tested on a previously unseen breadth of black-box optimization problems, ranging from academic benchmarks to real-world applications, from discrete over numerical to mixed-integer problems, from small to very large-scale problems, from noisy over dynamic to static problems, etc. Not only did we use the already very extensive benchmark environment available in Nevergrad, but we also extended it significantly by adding a number of additional benchmark suites, including Pyomo, Photonics, large-scale global optimization (LSGO), and MuJoCo. Our wizard achieves competitive performance on all benchmark suites. It significantly outperforms previous state-of-the-art algorithms on some of the suites, including YABBOB and LSGO. Its excellent performance is obtained without any task-specific parametrization. The algorithm selection wizard, all of its base solvers, as well as the benchmark suites are available for reproducible research in the open-source Nevergrad platform.
View PDF Chat

On the Partial Difference Equations of Mathematical Physics

1967-03-01
Richard Courant , Kurt Friedrichs , Hans Lewy
Problems involving the classical linear partial differential equations of mathematical physics can be reduced to algebraic ones of a very much simpler structure by replacing the differentials by difference quotients … Problems involving the classical linear partial differential equations of mathematical physics can be reduced to algebraic ones of a very much simpler structure by replacing the differentials by difference quotients on some (say rectilinear) mesh. This paper will undertake an elementary discussion of these algebraic problems, in particular of the behavior of the solution as the mesh width tends to zero. For present purposes we limit ourselves mainly to simple but typical cases, and treat them in such a way that the applicability of the method to more general difference equations and to those with arbitrarily many independent variables is made clear.

A Decision Procedure for Linear “Big O” Equations

2007-03-16
Jeremy Avigad , K. Donnelly
View PDF Chat

Star discrepancy subset selection: Problem formulation and efficient approaches for low dimensions

2022-01-11
François Clément , Carola Doerr , Luís Paquete
Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star … Motivated by applications in instance selection, we introduce the star discrepancy subset selection problem, which consists of finding a subset of m out of n points that minimizes the star discrepancy. First, we show that this problem is NP-hard. Then, we introduce a mixed integer linear formulation (MILP) and a combinatorial branch-and-bound (BB) algorithm for the star discrepancy subset selection problem and we evaluate both approaches against random subset selection and a greedy construction on different use-cases in dimension two and three. Our results show that the MILP and BB are efficient in dimension two for large and small m/n ratio, respectively, and for not too large n. However, the performance of both approaches decays strongly for larger dimensions and set sizes. As a side effect of our empirical comparisons we obtain point sets of discrepancy values that are much smaller than those of common low-discrepancy sequences, random point sets, and of Latin Hypercube Sampling. This suggests that subset selection could be an interesting approach for generating point sets of small discrepancy value.
View PDF Chat

Constructing low star discrepancy point sets with genetic algorithms

2013-07-06
Carola Doerr , François-Michel De Rainville
Geometric discrepancies are standard measures to quantify the irregularity of distributions. They are an important notion in numerical integration. One of the most important discrepancy notions is the so-called star … Geometric discrepancies are standard measures to quantify the irregularity of distributions. They are an important notion in numerical integration. One of the most important discrepancy notions is the so-called star discrepancy. Roughly speaking, a point set of low star discrepancy value allows for a small approximation error in quasi-Monte Carlo integration. It is thus the most studied discrepancy notion.
View PDF Chat

On the Partial Difference Equations of Mathematical Physics

2002-01-01
Richard Courant , Kurt Friedrichs , Hans Lewy
Problems involving the classical linear partial differential equations of mathematical physics can be reduced to algebraic ones of a very much simpler structure by replacing the differentials by difference quotients … Problems involving the classical linear partial differential equations of mathematical physics can be reduced to algebraic ones of a very much simpler structure by replacing the differentials by difference quotients on some (say rectilinear) mesh. This paper will undertake an elementary discussion of these algebraic problems, in particular of the behavior of the solution as the mesh width tends to zero. For present purposes we limit ourselves mainly to simple but typical cases, and treat them in such a way that the applicability of the method to more general difference equations and to those with arbitrarily many independent variables is made clear.

Certain Rational Functions Whose Power Series Have Positive Coefficients

1972-04-01
Richard Askey , George Gasper
(1972). Certain Rational Functions Whose Power Series Have Positive Coefficients. The American Mathematical Monthly: Vol. 79, No. 4, pp. 327-341. (1972). Certain Rational Functions Whose Power Series Have Positive Coefficients. The American Mathematical Monthly: Vol. 79, No. 4, pp. 327-341.
View PDF Chat

On the distribution of points in a cube and the approximate evaluation of integrals

1967-01-01
I. M. Sobol

Irregularities of distribution, VII

1972-01-01
Wolfgang Schmidt
View PDF Chat

Averages over hyperplanes, sum-product theory in vector spaces over finite fields and the Erdős-Falconer distance conjecture

2010-12-29
Derrick Hart , Alex Iosevich , Doowon Koh +1 more
We prove a pointwise and average bound for the number of incidences between points and hyperplanes in vector spaces over finite fields. While our estimates are, in general, sharp, we … We prove a pointwise and average bound for the number of incidences between points and hyperplanes in vector spaces over finite fields. While our estimates are, in general, sharp, we observe an improvement for product sets and sets contained in a sphere. We use these incidence bounds to obtain significant improvements on the arithmetic problem of covering <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper F Subscript q"> <mml:semantics> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>q</mml:mi> </mml:msub> <mml:annotation encoding="application/x-tex">{\mathbb F}_q</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, the finite field with <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="q"> <mml:semantics> <mml:mi>q</mml:mi> <mml:annotation encoding="application/x-tex">q</mml:annotation> </mml:semantics> </mml:math> </inline-formula> elements, by <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper A dot upper A plus midline-horizontal-ellipsis plus upper A dot upper A"> <mml:semantics> <mml:mrow> <mml:mi>A</mml:mi> <mml:mo>⋅</mml:mo> <mml:mi>A</mml:mi> <mml:mo>+</mml:mo> <mml:mo>⋯</mml:mo> <mml:mo>+</mml:mo> <mml:mi>A</mml:mi> <mml:mo>⋅</mml:mo> <mml:mi>A</mml:mi> </mml:mrow> <mml:annotation encoding="application/x-tex">A \cdot A+\dots +A \cdot A</mml:annotation> </mml:semantics> </mml:math> </inline-formula>, where <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="upper A"> <mml:semantics> <mml:mi>A</mml:mi> <mml:annotation encoding="application/x-tex">A</mml:annotation> </mml:semantics> </mml:math> </inline-formula> is a subset <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper F Subscript q"> <mml:semantics> <mml:msub> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> </mml:mrow> </mml:mrow> <mml:mi>q</mml:mi> </mml:msub> <mml:annotation encoding="application/x-tex">{\mathbb F}_q</mml:annotation> </mml:semantics> </mml:math> </inline-formula> of sufficiently large size. We also use the incidence machinery and develop arithmetic constructions to study the Erdős-Falconer distance conjecture in vector spaces over finite fields. We prove that the natural analog of the Euclidean Erdős-Falconer distance conjecture does not hold in this setting. On the positive side, we obtain good exponents for the Erdős-Falconer distance problem for subsets of the unit sphere in <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="double-struck upper F Subscript q Superscript d"> <mml:semantics> <mml:msubsup> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="double-struck">F</mml:mi> </mml:mrow> <mml:mi>q</mml:mi> <mml:mi>d</mml:mi> </mml:msubsup> <mml:annotation encoding="application/x-tex">\mathbb F_q^d</mml:annotation> </mml:semantics> </mml:math> </inline-formula> and discuss their sharpness. This results in a reasonably complete description of the Erdős-Falconer distance problem in higher-dimensional vector spaces over general finite fields.
View PDF Chat

Pinned distance sets, k-simplices, Wolff’s exponent in finite fields and sum-product estimates

2011-03-21
Jeremy Chapman , M. Burak Erdoğan , Derrick Hart +2 more
View PDF Chat

Numerical Partial Differential Equations: Finite Difference Methods

1995-01-01
J. W. Thomas

Adaptive step size random search

1968-06-01
M. Schumer , K. Steiglitz
Fixed step size random search for minimization of functions of several parameters is described and compared with the fixed step size gradient method for a particular surface. A theoretical technique, … Fixed step size random search for minimization of functions of several parameters is described and compared with the fixed step size gradient method for a particular surface. A theoretical technique, using the optimum step size at each step, is analyzed. A practical adaptive step size random search algorithm is then proposed, and experimental experience is reported that shows the superiority of random search over other methods for sufficiently high dimension.
View PDF Chat

The accuracy of the Gaussian approximation to the sum of independent variates

1941-01-01
Andrew Berry
The sum of finitely many variates possesses, under familiar conditions, an almost Gaussian probability distribution. This already much discussed central limit theorem(x) in the theory of probability is the object … The sum of finitely many variates possesses, under familiar conditions, an almost Gaussian probability distribution. This already much discussed central limit theorem(x) in the theory of probability is the object of further investigation in the present paper. The cases of Liapounoff(2), Lindeberg(3), and Feller(4) will be reviewed. Numerical estimates for the degrees of approximation attained in these cases will be presented in the three theorems of §4. Theorem 3, the arithmetical refinement of the general theorem of Feller, constitutes our principal result. As the foregoing implies, we require throughout the paper that the given variates be totally independent. And we consider only one-dimensional variates. The first three sections of the paper are devoted to the preparatory Theorem 1 in which the variates.meet the further condition of possessing finite third order absolute moments. Let X\, Xi, • • • , Xn be the given variates. For each k{k = \,2, ■ ■ ■ , n) let ^(Xk) and ixs{Xk) denote, respectively, the second and third order absolute moments of Xk about its mean (expected) value a*. These moments are either both zero or both positive. The former case arises only when Xk is essentially constant, i.e., differs from its mean value at most in cases of total probability zero. To avoid trivialities we suppose that PziXk) >0 for at least one k (k = 1, 2, • • • , n). The non-negative square root of m{Xk) is the standard deviation of Xk and will be denoted by ak. We call
View PDF Chat

Finite difference schemes and partial differential equations

1991-01-01
John C. Strikwerda
Preface to the second edition Preface to the first edition 1. Hyperbolic partial differential equations 2. Analysis of finite difference Schemes 3. Order of accuracy of finite difference schemes 4. … Preface to the second edition Preface to the first edition 1. Hyperbolic partial differential equations 2. Analysis of finite difference Schemes 3. Order of accuracy of finite difference schemes 4. Stability for multistep schemes 5. Dissipation and dispersion 6. Parabolic partial differential equations 7. Systems of partial differential equations in higher dimensions 8. Second-order equations 9. Analysis of well-posed and stable problems 10. Convergence estimates for initial value problems 11. Well-posed and stable initial-boundary value problems 12. Elliptic partial differential equations and difference schemes 13. Linear iterative methods 14. The method of steepest descent and the conjugate gradient method Appendix A. Matrix and vectoranalysis Appendix B. A survey of real analysis Appendix C. A Survey of results from complex analysis References Index.

On the efficiency of certain quasi-random sequences of points in evaluating multi-dimensional integrals

1960-12-01
John H. Halton

Application of Threshold-Accepting to the Evaluation of the Discrepancy of a Set of Points

1997-10-01
Peter Winker , Kai‐Tai Fang
Efficient routines for multidimensional numerical integration are provided by quasi--Monte Carlo methods. These methods are based on evaluating the integrand at a set of representative points of the integration area. … Efficient routines for multidimensional numerical integration are provided by quasi--Monte Carlo methods. These methods are based on evaluating the integrand at a set of representative points of the integration area. A set may be called representative if it shows a low discrepancy. However, in dimensions higher than two and for a large number of points the evaluation of discrepancy becomes infeasible. The use of the efficient multiple-purpose heuristic threshold-accepting offers the possibility to obtain at least good approximations to the discrepancy of a given set of points. This paper presents an implementation of the threshold-accepting heuristic, an assessment of its performance for some small examples, and results for larger sets of points with unknown discrepancy.
View PDF Chat

L-convergence paradox in numerical methods for PDEs

1991-03-01
Elemér E Rosinger

Leçons sur l'intégration et la recherche des fonctions primitives professées au Collège de France

2009-07-20
Henri Lebesgue
The two great works of the celebrated French mathematician Henri Lebesgue (1875–1941), Leçons sur l'intégration et la recherche des fonctions primitives professées au Collège de France (1904) and Leçons sur … The two great works of the celebrated French mathematician Henri Lebesgue (1875–1941), Leçons sur l'intégration et la recherche des fonctions primitives professées au Collège de France (1904) and Leçons sur les séries trigonométriques professées au Collège de France (1906) arose from lecture courses he gave at the Collège de France while holding a teaching post at the University of Rennes. In 1901 Lebesgue formulated measure theory; and in 1902 his new definition of the definite integral, which generalised the Riemann integral, revolutionised integral calculus and greatly expanded the scope of Fourier analysis. The Lebesgue integral is regarded as one of the major achievements in modern real analysis, and remains central to the study of mathematics today. Both of Lebesgue's books are reissued in this series.
View PDF Chat

Trusting computations: A mechanized proof from partial differential equations to actual program

2014-06-20
Sylvie Boldo , François Clément , Jean-Christophe Filliâtre +3 more
View PDF Chat

An Algorithm to Compute Bounds for the Star Discrepancy

2001-12-01
Eric Thiémard

Algorithm 647: Implementation and Relative Efficiency of Quasirandom Sequence Generators

1986-12-01
Bennett L. Fox
article Free AccessArtifacts Evaluated & ReusableArtifacts Available Share on Algorithm 647: Implementation and Relative Efficiency of Quasirandom Sequence Generators Author: Bennett L. Fox Computer Science Department, University of Montreal, P.O. … article Free AccessArtifacts Evaluated & ReusableArtifacts Available Share on Algorithm 647: Implementation and Relative Efficiency of Quasirandom Sequence Generators Author: Bennett L. Fox Computer Science Department, University of Montreal, P.O. Box 6128, Station A, Montreal, Quebec, Canada H3C 3J7 Computer Science Department, University of Montreal, P.O. Box 6128, Station A, Montreal, Quebec, Canada H3C 3J7View Profile Authors Info & Claims ACM Transactions on Mathematical SoftwareVolume 12Issue 4pp 362–376https://doi.org/10.1145/22721.356187Published:01 December 1986Publication History 117citation1,807DownloadsMetricsTotal Citations117Total Downloads1,807Last 12 Months78Last 6 weeks10 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF
View PDF Chat

A computer-verified monadic functional implementation of the integral

2010-06-11
Russell O’Connor , Bas Spitters
View PDF Chat

Adaptive Inexact Newton Methods with A Posteriori Stopping Criteria for Nonlinear Diffusion PDEs

2013-01-01
Alexandre Ern , Martin Vohralı́k
We consider nonlinear algebraic systems resulting from numerical discretizations of nonlinear partial differential equations of diffusion type. To solve these systems, some iterative nonlinear solver and, on each step of … We consider nonlinear algebraic systems resulting from numerical discretizations of nonlinear partial differential equations of diffusion type. To solve these systems, some iterative nonlinear solver and, on each step of this solver, some iterative linear solver are used. We derive adaptive stopping criteria for both iterative solvers. Our criteria are based on an a posteriori error estimate which distinguishes the different error components, namely, the discretization error, the linearization error, and the algebraic error. We stop the iterations whenever the corresponding error no longer affects the overall error significantly. Our estimates also yield a guaranteed upper bound on the overall error at each step of the nonlinear and linear solvers. We prove the (local) efficiency and robustness of the estimates with respect to the size of the nonlinearity owing, in particular, to the error measure involving the dual norm of the residual. Our developments hinge on equilibrated flux reconstructions and yield a general framework. We show how to apply this framework to various discretization schemes like finite elements, nonconforming finite elements, discontinuous Galerkin, finite volumes, and mixed finite elements; to different linearizations like fixed point and Newton; and to arbitrary iterative linear solvers. Numerical experiments for the $p$-Laplacian illustrate the tight overall error control and important computational savings achieved in our approach.
View PDF Chat

Introduction to Nonparametric Estimation

2008-10-21
Alexandre B. Tsybakov

Recent Progress in Improvement of Extreme Discrepancy and Star Discrepancy of One-Dimensional Sequences

2009-01-01
Victor Ostromoukhov

Covering numbers, dyadic chaining and discrepancy

2011-03-11
Christoph Aistleitner

Component-by-component construction of low-discrepancy point sets of small size

2008-07-01
Benjamin Doerr , Michael Gnewuch , Peter Kritzer +1 more
Abstract We investigate the problem of constructing small point sets with low star discrepancy in the s -dimensional unit cube. The size of the point set shall always be polynomial … Abstract We investigate the problem of constructing small point sets with low star discrepancy in the s -dimensional unit cube. The size of the point set shall always be polynomial in the dimension s . Our particular focus is on extending the dimension of a given low-discrepancy point set. This results in a deterministic algorithm that constructs N -point sets with small discrepancy in a component-by-component fashion. The algorithm also provides the exact star discrepancy of the output set. Its run-time considerably improves on the run-times of the currently known deterministic algorithms that generate low-discrepancy point sets of comparable quality. We also study infinite sequences of points with infinitely many components such that all initial subsegments projected down to all finite dimensions have low discrepancy. To this end, we introduce the inverse of the star discrepancy of such a sequence, and derive upper bounds for it as well as for the star discrepancy of the projections of finite subsequences with explicitly given constants. In particular, we establish the existence of sequences whose inverse of the star discrepancy depends linearly on the dimension.
View PDF Chat

On irregularities of distribution

1954-12-01
K. F. Roth

Good permutations for deterministic scrambled Halton sequences in terms of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" altimg="si69.gif" overflow="scroll"><mml:msub><mml:mrow><mml:mi>L</mml:mi></mml:mrow><mml:mrow><mml:mn>2</mml:mn></mml:mrow></mml:msub></mml:math>-discrepancy

2005-07-28
Bart Vandewoestyne , Ronald Cools