Depth Separation for Neural Networks under Gaussian Measure
Cynthia Bortolotto, Francisco Ganacim, Roberto I. Oliveira
stat.ML
Oct 20, 2026 · v1
cs.LG
TL;DR
All theorems, lemmas, propositions and corollaries are formalized in Lean 4 with Mathlib, developed with LLM assistance and checked by an axiom audit.
Abstract
We revisit the problem of depth separation for neural networks, as studied by Eldan and Shamir, Daniely, and others. Specifically, we consider the natural setting of $L^2$ approximation of radial functions under the standard Gaussian measure in $d$ dimensions. We show that there is a radial function in $L^2$ under the standard Gaussian measure that can be approximated to a fixed sufficiently small $L^2$ error by a depth-3 ReLU neural network of polynomial size in $d$ but can only be approximated by depth-2 networks with subexponentially bounded weights if their size is at least exponential in $d$. For that, we prove a general result showing that if a radial function has substantial mass in the high frequencies of its Hermite expansion, then it cannot be well approximated by a depth-2 neural network with small width and bounded weights. All theorems, lemmas, propositions, and corollaries are verified in Lean 4.
Problem
The work revisits depth separation for neural networks in the natural setting of L^2 approximation of radial functions under the standard Gaussian measure in d dimensions. Earlier separations relied on tailored measures or other distributions.
Approach
Hermite expansions, Gaussian chaos projections and radialization of ridge functions are used to prove that radial functions with substantial high-frequency Hermite mass cannot be well approximated by narrow depth-2 networks with bounded weights. An oscillatory radial function sin(4π√d‖x‖²) is then shown to be approximable by a polynomial-size depth-3 ReLU network. All results are formalized in Lean 4 using Mathlib, with LLM assistance (Claude, GPT), and the statements were audited by the authors.
Results
There is a radial function that a polynomial-size depth-3 ReLU network approximates to small fixed L^2 error, while depth-2 networks with subexponentially bounded weights need exponential size. The Lean development builds with only the standard axioms propext, Classical.choice and Quot.sound, and has no admitted proofs or project-defined axioms.
