15 citations · 38 across the 8 of their papers we have counts for
10 papers
Carleson operators on doubling metric measure spaces
Lars Becker, Floris van Doorn, Asgar Jamneshan +2
Doubling metric measure spaces provide a natural framework for singular integral operators. In contrast, the study of maximally modulated singular integral operators, the so-called…
Formalising the -principle and sphere eversion
Patrick Massot, Floris van Doorn, Oliver Nash
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existen…
Designing a general library for convolutions
Floris van Doorn
We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applica…
Formalized Haar Measure
Floris van Doorn
We describe the formalization of the existence and uniqueness of Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups…
A Formal Proof of the Independence of the Continuum Hypothesis
Jesse Michael Han, Floris van Doorn
We describe a formal proof of the independence of the continuum hypothesis () in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for bo…
Maintaining a Library of Formal Mathematics
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors…