Shallow Learning Tends to Ridgelet Transform

Sho Sonoda

A Lean 4 formalization of the paper Shallow Learning Tends to Ridgelet Transform (arXiv:XXXX.XXXXX): conditions under which a finite shallow neural network trained by regularized (mean-field Langevin) learning converges to the continuous ridgelet transform of the target function. It covers the structure theorem for the Gibbs minimizer (M1: the mean amplitude is a regularized ridgelet transform), the mean-field Langevin convergence and static chaos, the sample-size threshold (M3), the regularization limit to the canonical ridgelet transform and the order of limits (M4), and the convergence rates under source conditions. Built on Mathlib and lean-operator-ridgelet.

Status (2026-09-27): 44,312 lines of Lean, 919 blueprint nodes. Every main theorem depends only on propext, Classical.choice and Quot.sound (116 statements verified by Comparator); seven cited or auxiliary facts (Gaussian log-Sobolev inequality, SDE well-posedness, Łojasiewicz, the trace identity and min-max identification of the limit spectrum, the arcsine kernel) remain sorry and are not on the main chain. Sections 2, 3, 5, 6, 10, 12, the circle case of Section 11 and the non-stochastic part of Section 4 are formalized; Section 9, the homogeneous geometry of Section 11 and the propagation-of-chaos part of Section 4 are not.

• BlueprintStatements, proofs and their Lean status
• Dependency graphWhat depends on what, and what is done
• Blueprint (PDF)Printable version
• Comparator certificateChallenge statements and the latest verification result
• Source codeLean project on GitHub