Journées FastRelax

05-07 Juin 2018

La réunion a eu lieu au centre Inria de Sophia Antipolis, en salle Coriolis (Bâtiment Galois). Comment venir ?

Programme provisoire

Mardi 5 Juin

Possibilité de déjeuner sur place.
14:00
Accueil
14:30
Florian Steinberg
15:00
Florent Bréhard, A computer-assisted proof for a new lower bound on H(4) in Hilbert's sixteenth problem (joint work with N. Brisebarre and W. Tucker)
15:30
Pause
16:00
Marc Mezzarobba, Truncation Bounds for Differentially Finite Series
16:30
Laurent Théry
17:00
Discussions

Mercredi 06 Juin

9:30
Paul Zimmermann, On various ways to split a floating-point number (joint work with Jean-Michel Muller et Claude-Pierre Jeannerod)
10:30
Pause
11:00
Manuel Eberl, Semi-Automatic Real Asymptotics in Isabelle/HOL
11:30
Cyril Cohen, Analysis in Mathcomp: o and O
12:00
Déjeuner
14:00
Mioara Joldes et Denis Arzelier, Global Probability of Collision (joint works with F. Bréhard, J.-B. Lasserre and A. Rondepierre)
  1. Problem modeling via occupation measures
  2. On a moment inverse problem with D-finite functions
15:30
Pause
16:00
Damien Roughling , Formal Proofs for Control and Robotics: A Case Study
16:30
Discussions : Prolongation FastRelax
19:30
Dîner au restaurant "Les vieux murs" à Antibes

Jeudi 7 Juin

9:30
Pascal Molin, Périodes de courbes ???
10:10
Fredrik Johansson, Numerical integration in arbitrary-precision ball arithmetic
10:30
Yves Bertot
10:50
Pause
11:10
Bruno Salvy , Generalized Hermite Reduction, Creative Telescoping and Definite Integration of D-Finite Functions
11:40
Erik Martin-Dorel, Experiments about global optimization (tentative title)
12:30
Fin des rencontres

Résumés

Marc Mezzarobba, Truncation Bounds for Differentially Finite Series

I will present a flexible symbolic-numeric algorithm for computing bounds on the remainders of series solutions of linear ODEs with polynomial coefficients. Such bounds are useful in rigorous numerics, typically in rigorous versions of the Taylor method of numerical integration of ODEs. The algorithm fully covers the case of generalized series expansions at regular singular points. It is a key part of the rigorous Taylor method implemented in the Sage package ore_algebra, and experiments with the implementation show that it yields tight bounds in practice at an acceptable computational cost, even for equations of high order with coefficients of large degree.

Paul Zimmermann, On various ways to split a floating-point number

We review several ways to split a floating-point number, that is, to decompose it into the exact sum of two floating-point numbers of smaller precision. All the methods considered here involve only a few floating-point operations with rounding to nearest, including possibly the fused multiply-add (FMA). Applications range from the implementation of integer functions such as floor or round to ``scaling'' of calculations (such as sqrt(a^2+b^2)) to avoid spurious underflow and overflow.

This is a joint work with Claude-Pierre Jeannerod and Jean-Michel Muller.

Manuel Eberl, Semi-Automatic Real Asymptotics in Isabelle/HOL

Computer Algebra Systems can easily compute limits and asymptotic expansions of complicated real functions; interactive theorem provers, on the other hand, provide very little support for such problems and proving asymptotic properties of a function often involves long and tedious manual proofs.

In this talk, I will present my work about bringing automation for real-valued asymptotics to Isabelle/HOL using multiseries expansions. This yields a procedure to automatically prove limits and ‘Big-O' estimates of real-valued functions similarly to computer algebra systems like Mathematica and Maple – but while proving every step of the process correct.

Fredrik Johansson. Numerical integration in arbitrary-precision ball arithmetic.

We discuss arbitrary-precision numerical integration with rigorous error bounds in the framework of ball arithmetic. A new implementation has recently been added to the Arb library. Rapid convergence is ensured for piecewise complex analytic integrals by use of the Petras algorithm, which combines adaptive bisection with degree-adaptive Gaussian quadrature where error bounds are determined via complex magnitudes without evaluating derivatives. The code is general, easy to use, and efficient, often outperforming existing non-rigorous software.

Florent Bréhard. A computer-assisted proof for a new lower bound on H(4) in Hilbert's sixteenth problem

We provide a computer-assisted proof for a new lower bound on H(4) in the Hilbert 16th problem, that is the maximum number of limit cycles that can occur in a polynomial planar vector field of degree 4. Indeed, we exhibit a quartic vector field for which we rigorously prove the existence of at least 24 limit cycles. Hilbert's 16th problem is part of Hilbert's famous list of 23 problems presented in 1900 at the International Congress of Mathematicians in Paris. The second part of this problem asks whether there exists, for each natural integer n, a finite upper bound H(n) on the number of limit cycles a polynomial planar vector field of degree n can have. For now, a proof of this conjecture seems out of reach, even for n = 2. A simpler version of this problem restricts the investigation to perturbed Hamiltonian systems. The upper bound Z(n) for such systems of degree n was proved to be finite for all n. A key ingredient is the Poincaré-Pontryagin theorem that relates the number of limit cycles with the number of zeros of so-called Abelian integrals along the level curves of the potential function associated to the Hamiltonian system.

The quartic system we investigate is not Hamiltonian but still integrable, so that the Poincaré-Pontryagin theorem still applies. Our work consists in approximating the Abelian integral associated to each monomial of the perturbation (as function of the energy level of the potential function), adjusting the coefficients to maximize the number of zeros of the resulting linear combination, and finally computing rigorous enclosures of the integral at various points to certify the number of sign changes. For that purpose, we use Rigorous Polynomial Approximations [1,2,3] via our free C library available here [4], which allows us to perform rigorous and efficient evaluations of the Abelian integral.

A formalization of this result in Coq is in progress, in order to avoid possible implementation errors that may lead to a wrong result. This is a joint work with Nicolas Brisebarre and Warwick Tucker.