80 citations · 87 across the 7 of their papers we have counts for
9 papers
Higher order differential calculus in mathlib
Sébastien Gouëzel
We report on the higher-order differential calculus library developed inside the Lean mathematical library mathlib. To support a broad range of applications, we depart in several w…
A formalization of the change of variables formula for integrals in mathlib
Sébastien Gouëzel
We report on a formalization of the change of variables formula in integrals, in the mathlib library for Lean. Our version of this theorem is extremely general, and builds on devel…
Formalizing the Gromov-Hausdorff space
Sébastien Gouëzel
The Gromov-Hausdorff space is usually defined in textbooks as "the space of all compact metric spaces up to isometry". We describe a formalization of this notion in the Lean proof…
Asymptotic combinatorics of Artin-Tits monoids and of some other monoids
Samy Abbes, Sébastien Gouëzel, Vincent Jugé +1
We introduce methods to study the combinatorics of the normal form of large random elements in Artin-Tits monoids. These methods also apply in an axiomatic framework that encompass…
A corrected quantitative version of the Morse lemma
Sébastien Gouëzel, Vladimir Shchur
There is a gap in the proof of the main theorem in the article [ShCh13a] on optimal bounds for the Morse lemma in Gromov-hyperbolic spaces. We correct this gap, showing that the ma…
Variations around Eagleson's Theorem on mixing limit theorems for dynamical systems
Sébastien Gouëzel
Eagleson's Theorem asserts that, given a probability-preserving map, ifrenormalized Birkhoff sums of a function converge in distribution, thenthey also converge with respect to any…