Lean 4 / Mathlib formalizations of results from my research, with the proofs checked by the Lean kernel.
Projects
A formalization states definitions and theorems in the dependent type theory of Lean 4 and gives their proofs as terms of that theory. Whether such a term is a proof is decided by a small kernel that rechecks every step, and the axioms a finished proof relies on can be listed exactly. Mathlib, the community library, supplies the underlying analysis, linear algebra and topology basics, and is extended over time.
The projects are hosted on GitHub. Each comes with a blueprint, a readable account of the mathematics with links into the Lean code, and a dependency graph showing which results rest on which.
Palomar is a public registry of Lean formalizations. It re-runs the proof itself at one pinned commit of the repository and records the outcome, down to the axioms the proof rests on.
Blueprint (as pdf)·Dependency graph·
Dependency graphPietsch's axiomatic theory of s-numbers, which takes the place of the singular values on Banach spaces, where no spectral theorem is at hand. The development covers the axioms, the five classical sequences (the approximation numbers \(a_n\), the Bernstein, Gelfand and Kolmogorov numbers, and the Hilbert numbers \(h_n\)) and the inequalities between them. Its main result is the maximal difference theorem \(a_n(S)\le e(n+1)\,h_n(S)\). Since \(a_n\) is the largest s-number sequence and \(h_n\) the smallest, this single factor bounds the gap between any two of them, and its growth in \(n\) is order-optimal.
Getting there called for a good deal of general functional analysis that Mathlib does not yet carry: Auerbach's lemma, John's ellipsoid together with the decomposition of the identity, the singular value decomposition of a compact operator, the Eckart–Young theorem, and the projection theorems of Kadets–Snobar and Garling–Gordon.
Registered in Palomar
SNumbers.approximationNumber_le_mul_hilbertNumber\(a_n(S)\le \frac{(n+1)^{n+1}}{n^{n}}\,h_n(S)\)SNumbers.approximationNumber_le_e_mul_hilbertNumber\(a_n(S)\le e\,(n+1)\,h_n(S)\)Blueprint (as pdf)·Dependency graph·
Dependency graphTwo theorems that replace a norm by finitely many point evaluations. The first is the generalized sparsification theorem of Batson, Spielman and Srivastava from a joint paper with Chkifa, Dolbeault and Krieg: for an \(m\)-dimensional space of square-integrable functions and every \(n\ge m\) there are \(n\) points and positive weights such that \(\sum_i w_i\,|f(x_i)|^2\) stays within the factors \((1\mp\sqrt{(m-1)/n})^2\) of \(\int|f|^2\,d\mu\) for every \(f\) in the space, with no side condition. In the generalized form the upper bound refers to a second family, which may be countably infinite, and depends on its effective dimension rather than its size; this is what makes the theorem applicable to reproducing kernel Hilbert spaces.
The second is the Kiefer–Wolfowitz theorem in the form used for sampling projections: on an \(m\)-dimensional space of bounded functions, a probability measure maximizing the determinant of the Gram matrix bounds the uniform norm by the \(L_2\) norm with the constant \(\sqrt{m+\varepsilon}\), and with \(\sqrt{m}\) on a compact domain. Both proofs are constructive. Among the building blocks Mathlib does not yet carry are Sherman–Morrison for rank-one updates, the matrix determinant lemma and the trace of an operator along a Hilbert basis.
Registered in Palomar
Discretization.bss\((1-\sqrt{(m-1)/n})^2 I \preceq \sum_i w_i\,a(x_i)a(x_i)^* \preceq (1+\sqrt{(m-1)/n})^2 I\)Discretization.bss_of_sum_eq_one\((1-\sqrt{(m-1)/n})^2 I \preceq \sum_k s_k\,v_k v_k^* \preceq (1+\sqrt{(m-1)/n})^2 I\)