5. Mathlib upstream candidates
This chapter collects the general-purpose results developed for the ridgelet formalization and staged for upstreaming to Mathlib. They import only Mathlib and carry no dependence on the ridgelet theories.
The sections are separate Lean modules and cache boundaries: Lp and measure transport; Radon
and Fourier transforms; supporting integral and Fourier tools; Schwartz space and convolution;
finite Fourier and Euclidean geometry; unitary representations and topological groups; invariant
geometry and integration; and symmetric spaces with the Helgason--Fourier transform. A change in
one independent topic therefore leaves the unrelated Blueprint section objects reusable.
A survey of the pinned Mathlib version confirmed the principal gaps represented here. Mathlib has
no Radon or d-plane transform, Fourier slice theorem, Hilbert transform, general Young
convolution inequality on Lp, or matrix polar integration formula. The child sections state the
precise generality and proof strategy of each upstream candidate.
- 5.1. Mathlib candidates: Lp and measure transport
- 5.2. Mathlib candidates: Radon and Fourier transforms
- 5.3. Mathlib candidates: integral and Fourier tools
- 5.4. Mathlib candidates: Schwartz space and convolution
- 5.5. Mathlib candidates: finite Fourier and Euclidean geometry
- 5.6. Mathlib candidates: unitary representations and groups
- 5.7. Mathlib candidates: invariant geometry and integration
- 5.8. Mathlib candidates: symmetric spaces and the Helgason--Fourier transform