Computer-assisted proofs, proof assistants and visualization in dynamical systems
from
Tuesday, 18 June 2024 (08:30)
to
Friday, 21 June 2024 (14:00)
Monday, 17 June 2024
Tuesday, 18 June 2024
08:30
Registration
Registration
08:30 - 09:00
09:00
Tucker, Warwick
-
Tucker Warwick
(
Monash University
)
Tucker, Warwick
Tucker Warwick
(
Monash University
)
09:00 - 09:50
Lower bounds on the Hausdorff dimensions of Julia sets Abstract: We present an algorithm for a rigorous computation of lower bounds on the Hausdorff dimensions of Julia sets for a wide class of holomorphic maps. We apply this algorithm to obtain lower bounds on the Hausdorff dimension of the Julia sets of some infinitely renormalizable real quadratic polynomials, including the Feigenbaum polynomial $p{\textrm{Feig}}(z) = z2 + c{\textrm{Feig}}$ . In addition to that, we construct a piecewise constant function on $-2, 2$ that provides rigorous lower bounds for the Hausdorff dimension of the Julia sets of all quadratic polynomials $pc (z) = z2 + c$ with $c \in -2, 2$. Finally, we verify the conjecture of Ludwik Jaksztas and Michel Zinsmeister that the Hausdorff dimension of the Julia set of a quadratic polynomial $pc (z) = z2 + c$, is a $C1$-smooth function of the real parameter c on the interval $c \in (c{\textrm{Feig}} ,-34)$.
09:50
Cofee Break
Cofee Break
09:50 - 10:10
10:10
"Rigorous enclosure of the discrete spectrum for transfer operators"
-
Isaia Nisoli
(
Universidade Federal de Rio de Janeiro
)
"Rigorous enclosure of the discrete spectrum for transfer operators"
Isaia Nisoli
(
Universidade Federal de Rio de Janeiro
)
10:10 - 11:00
abstract: In this work, in collaboration with Blumenthal and Taylor-Crush, I present a generalization of a fundamental result, the Gerschgorin circle theorem, to obtain enclosures of the discrete spectrum of a transfer operator preserving a strong Banach space compactly embedded in a weak Banach space. The enclosures are obtained by rigorously bounding the weak resolvent norm of a finite rank approximation of the transfer operator. This result has important consequences, allowing us to understand the finer statistical properties of systems satisfying a Lasota-Yorke inequality, as uniformly expanding maps and systems with additive noise.
11:00
Discussion and self organized collaboration
Discussion and self organized collaboration
11:00 - 11:50
12:00
Lunch
Lunch
12:00 - 15:30
15:30
The Lean theorem prover
-
Sébastien Gouëzel
(
CNRS and Université de Rennes
)
The Lean theorem prover
Sébastien Gouëzel
(
CNRS and Université de Rennes
)
15:30 - 16:20
Interactive theorem provers are a kind of programming languages in which one explains proofs to a computer in a formal language, where the computer checks that the proof respects the rules of logic. I will present the Lean theorem prover, together with its mathematics library Mathlib. This library is advanced enough that one may start to formalize complicated statements in dynamics (and all other areas of mathematics!)
16:20
Cofee Break
Cofee Break
16:20 - 16:40
16:40
Spectra of transfer and Koopman operators
-
Julia Slipantschuk
(
University of Warwick
)
Spectra of transfer and Koopman operators
Julia Slipantschuk
(
University of Warwick
)
16:40 - 17:30
This talk will be about computation and approximation of spectral data of transfer operators and Koopman operators associated to holomorphic expanding and hyperbolic discrete dynamical systems. I will present a special class of systems with explicitly computable eigenvalues. In a more general setting, I will discuss convergence results of algorithms such as Lagrange-Chebyshev or EDMD to approximate spectral data and obtain rigorous bounds in various applications.
17:30
Discussion and self organized collaboration
Discussion and self organized collaboration
17:30 - 18:30
Wednesday, 19 June 2024
09:00
Machine learning of Hamiltonian dynamical systems
-
Hongkun Zhang
(
University of Massachusetts Amherst
)
Machine learning of Hamiltonian dynamical systems
Hongkun Zhang
(
University of Massachusetts Amherst
)
09:00 - 09:50
n recent years, machine learning algorithms have emerged as powerful tools for modeling and understanding dynamical systems. This talk presents an overview of the recent advancements in machine learning of Hamiltonian dynamical systems. I discuss machine learning techniques that we have successfully applied to learn conservation laws for certain nonlinear lattice systems. Furthermore, we highlight the challenges and considerations in applying machine learning to dynamical systems, especially chaotic systems.
09:50
Cofee Break
Cofee Break
09:50 - 10:10
10:10
Explicit resolvent bounds for transfer operators
-
Oscar Bandtlow
(
Queen Mary University of London
)
Explicit resolvent bounds for transfer operators
Oscar Bandtlow
(
Queen Mary University of London
)
10:10 - 11:00
In this talk I will explain how to obtain explicit upper bounds for the resolvent R(z,L) of any compact operator L on a Hilbert space in terms of its singular values and the distance of z to the spectrum of L. I will then discuss applications of this estimate to obtaining explicit a priori error bounds for spectral approximations of transfer operators. Time permitting, I will also explain how to extend these results to the Banach space setting.
11:00
Discussion and self organized collaboration
Discussion and self organized collaboration
11:00 - 11:50
12:00
Lunch
Lunch
12:00 - 15:30
15:30
Estimates on Lyapunov exponents via the pressure function
-
Mark Pollicott
(
University of Warwick
)
Estimates on Lyapunov exponents via the pressure function
Mark Pollicott
(
University of Warwick
)
15:30 - 16:20
Given an expanding map of the interval one can estimate the Lyapunov exponent (or equivalently the metric entropy) for the absolutely continuous invariant probability measure using the pressure function. This lends itself to rigorous estimates. For random products of suitable matrices the same approach gives estimates on their top Lyapunov exponent.
16:20
Cofee Break
Cofee Break
16:20 - 16:40
16:40
Computing and visualizing measures with maximum entropy and other equilibrium states
-
Jerome Buzzi
(
Université Paris-Saclay
)
Computing and visualizing measures with maximum entropy and other equilibrium states
Jerome Buzzi
(
Université Paris-Saclay
)
16:40 - 17:30
One generally expects SRB measures to match in some way direct simulations of dynamical systems (even though making the corresponding mathematical statement is far from easy). My goal is to draw attention to the problem of computing more abstract objects such as measures maximizing the entropy and more generally equilibrium states. I will recall some old and new results suggesting motivations, possible approaches, and highlighting some difficulties.
Thursday, 20 June 2024
09:00
Two classes of highly effective discretisations
-
Caroline Wormell
(
Australian National University
)
Two classes of highly effective discretisations
Caroline Wormell
(
Australian National University
)
09:00 - 09:45
Chebyshev and Fourier approximation are effective and now well-used ways to discretise analytic full-branch uniformly expanding dynamics. They are simple, easy to implement and clearly have a lot of room to be extended. This talk will present two such extensions. The first looks to the burgeoning applied area of Koopman operator numerics, where Koopman operators are approximated by least-squares with respect to a general sampling measure (e.g. the SRB measure). I will show that for trigonometric function dictionaries that this discretisation is nearly as accurate as Fourier Galerkin methods, and fairly good estimates can be even obtained purely from time series data, when done carefully. The second will be to approximate Koopman or transfer operators of analytic hyperbolic maps (and more generally Anosov maps). This enables rigorous and highly accurate estimates of spectral data, including of general Anosov flows.
09:50
Cofee Break
Cofee Break
09:50 - 10:10
10:10
High performance computing on a teapot
-
Alexey Korepanov
(
Loughborough University
)
High performance computing on a teapot
Alexey Korepanov
(
Loughborough University
)
10:10 - 11:00
I'll talk about portability and presentation of numerical results and simulations. In particular, about stable workflow that works in extreme universality, relying on most widely installed and used program: your browser. This is a popular talk without any serious mathematical content.
11:00
Common work
Common work
11:00 - 11:50
12:00
Lunch
Lunch
12:00 - 15:00
15:00
Common work
Common work
15:00 - 16:40
16:40
Cofee Break
Cofee Break
16:40 - 17:00
17:00
Round table on visualization (Chairman: JR Chazottes)
Round table on visualization (Chairman: JR Chazottes)
17:00 - 17:50
17:50
Discussion and self organized collaboration
Discussion and self organized collaboration
17:50 - 18:20
Friday, 21 June 2024
09:00
Dimension function of the Lagrange and Markov spectra
-
Polina Vytnova
(
University of Surrey
)
Dimension function of the Lagrange and Markov spectra
Polina Vytnova
(
University of Surrey
)
09:00 - 09:50
I will discuss an approach for computing the Hausdorff dimension of an intersection of the classical Lagrange and Markov spectra with half-infinite ray d(t) = dim(M \cap (−∞,t)), that allows to plot a graph of the function d(t) with high accuracy. The talk is based on a recent joint work with Carlos Gustavo Moreira and Carlos Matheus Santos (arxiv:2212.11371).
09:50
Cofee Break
Cofee Break
09:50 - 10:10
10:10
Formalizing topological entropy in Lean
-
Damien Thomine
(
Université Paris-Saclay
)
Formalizing topological entropy in Lean
Damien Thomine
(
Université Paris-Saclay
)
10:10 - 11:00
I will present a project to formalize some elements of topological dynamics in Lean, and its current advancement. A special emphasis will be given to many design decisions, and how they arise from the interaction between a well-established mathematical theory and a proof assistant.
11:00
Final Round Table
Final Round Table
11:00 - 11:50
11:50
Lunch
Lunch
11:50 - 14:00