21 citations · 21 across the 3 of their papers we have counts for
5 papers
Formalizing Carleson's Theorem in Lean
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +11
We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the m…
A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +14
This paper is the blueprint underlying the Lean formalization of the proof of Carleson's classical result asserting almost everywhere convergence of Fourier series of continuous fu…
Progress on a perimeter surveillance problem
Jeremy Avigad, Floris van Doorn
We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, drones surve…
Homotopy Type Theory in Lean
Floris van Doorn, Jakob von Raumer, Ulrik Buchholtz
We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of jus…
Constructing the Propositional Truncation using Non-recursive HITs
Floris van Doorn
In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recur…