2. Neural networks with Hilbert-space inputs
A network measures its input through inner products and applies a scalar activation to
those measurements. The input space H is a separable real Hilbert space; the output
space Y is a separable complex Hilbert space. Approximation is measured uniformly on
compact input sets. Finite-width networks are obtained by sampling an integral network.
The statements below use the bias coordinate c=-b, so that a manuscript neuron
\sigma(\langle a,x\rangle-b) is written \beta(\langle a,x\rangle+c).
This coordinate choice agrees with the Lean statements and leaves the represented networks unchanged.