Computer-assisted proofs, proof assistants and visualization in dynamical systems

Contribution List

2. Tucker, Warwick

Dr Tucker Warwick (Monash University)

18/06/2024, 09:00

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...

3. "Rigorous enclosure of the discrete spectrum for transfer operators"

Dr Isaia Nisoli (Universidade Federal de Rio de Janeiro)

18/06/2024, 10:10

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...

4. The Lean theorem prover

Prof. Sébastien Gouëzel (CNRS and Université de Rennes)

18/06/2024, 15:30

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...

5. Spectra of transfer and Koopman operators

Prof. Julia Slipantschuk (University of Warwick)

18/06/2024, 16:40

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...

6. Machine learning of Hamiltonian dynamical systems

Prof. Hongkun Zhang (University of Massachusetts Amherst)

19/06/2024, 09:00

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...

7. Explicit resolvent bounds for transfer operators

Oscar Bandtlow (Queen Mary University of London)

19/06/2024, 10:10

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...

8. Estimates on Lyapunov exponents via the pressure function

Mark Pollicott (University of Warwick)

19/06/2024, 15:30

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.

9. Computing and visualizing measures with maximum entropy and other equilibrium states

Jerome Buzzi (Université Paris-Saclay)

19/06/2024, 16:40

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,...

10. Two classes of highly effective discretisations

Caroline Wormell (Australian National University)

20/06/2024, 09:00

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...

11. High performance computing on a teapot

Alexey Korepanov (Loughborough University)

20/06/2024, 10:10

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.

12. Dimension function of the Lagrange and Markov spectra

Polina Vytnova (University of Surrey)

21/06/2024, 09:00

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).

13. Formalizing topological entropy in Lean

Damien Thomine (Université Paris-Saclay)

21/06/2024, 10:10

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.