1.4. Notation and organization🔗

Unless otherwise stated, H is an infinite-dimensional separable real Hilbert space, Y is a separable complex Hilbert space, and P,Q are injective positive self-adjoint trace-class operators. Functions are complex valued unless a real activation or output is specified. The one-dimensional Fourier convention is h^\sharp(\omega)=\int h(t)e^{-it\omega}\,\mathrm dt and h(t)=(2\pi)^{-1}\int h^\sharp(\omega)e^{it\omega}\,\mathrm d\omega. We use \sharp for one-dimensional and partial bias transforms and \widehat{\phantom f} for spatial Fourier–Stieltjes transforms and torus coefficients. Distributional pairings are bilinear.

The manuscript uses b and \sigma; the formal statements and the mathematical nodes below use c=-b and \beta. They use the same spatial symbol F_Q and often G for a spectral density g. These are changes of coordinates and notation, not changes in the network or theorem hypotheses.

Sections 2–7 develop the definitions, analysis, reconstruction, activations, approximation and examples, with their prerequisites and proofs supplied before use. Section 8 reports numerical experiments and Section 9 discusses computation and open questions. Appendix A gives a kernel interpretation, B gives coefficient projections, C gives additional approximation bounds, D compares finite-dimensional formulas and explains the dilation obstruction, E gives numerical methods, and F is an extended overview of related work.

Each numbered result links to its Lean declarations. The L^2 clause of Theorem 5.10 and the closed-form reconstruction constants of Proposition 5.12 are carried in weaker forms by the Lean statements. The formalization infrastructure is documented separately after the manuscript chapters.