7. Further results from the source manuscript
The following results appear in the arXiv src/03dev-*.tex files but lie beyond the current
formalization of Chapters 2--5. They are recorded as unformalized nodes with their dependencies
made explicit.
- No associated Lean code or declarations.
A countable family of L^2 functions can be encoded isometrically into an orthonormal sequence
in the null fiber. A suitable additive parameter perturbation reads a selected function into the
visible component without changing the null component, and this perturbation is the unique one of
minimum norm.
For a finite complex Radon measure \mu and a localized data measure \nu, define the
measure-valued synthesis S_\nu[\mu] as the Bochner integral of the feature map.
A null measure of total variation one can be approximated by an atomic measure of width N,
whose output norm converges to zero at rate O(N^{-1/2}).
Uniform Monte Carlo sampling on a bounded parameter domain for a finite measure separates the
truncation error from the sampling error, and the latter has mean square O(N^{-1}).
For a continuous activation of at most polynomial growth and a compactly supported data measure, every Schwartz ridgelet null element yields a finite-width null approximation.
- No associated Lean code or declarations.
The parity of an activation gives an exact two-atom null relation. For ReLU, affine cancellation conditions give further exact null relations among finitely many neurons.