IEEE32Exec two-layer ReLU approximation bound #
This file proves the reusable three-term error decomposition for executing a single-hidden-layer ReLU MLP under concrete IEEE binary32 semantics.
The theorem separates the three mathematically different sources of error:
- real approximation: the ideal real-valued ReLU MLP approximates the target,
- parameter quantization: the real MLP is close to the real interpretation of the IEEE parameters, and
- IEEE execution: the executable graph, interpreted back into $\mathbb{R}$, is close to the real graph with those interpreted parameters.
This is the finite-dimensional analogue of the hinge-network executable bound in
UniversalApproximationIEEE32Exec. The decomposition follows the standard numerical-analysis
pattern for floating-point algorithms: prove the real algorithm correct, bound data/parameter
rounding, and bound arithmetic rounding separately. For background, see IEEE Std 754-2019,
Goldberg (1991), Higham (2002), and the ReLU density literature of Cybenko, Hornik, Leshno, and
Pinkus.
Three-term bound #
Read this as:
Given an IEEE32Exec input xI, let $x_R$ be its real interpretation (toReal elementwise).
If:
- the target $f$ is approximated by a real two-layer ReLU MLP with error at most $\varepsilon_{\mathrm{approx}}$,
- the real MLP is close to the real interpretation of the IEEE parameters, with error at most $\varepsilon_Q$,
- executing the IEEE MLP and then mapping to reals is close to the real interpretation of those IEEE parameters, with error at most $\varepsilon_R$,
then the IEEE32Exec execution approximates $f$ within $\varepsilon_{\mathrm{approx}}+\varepsilon_Q+\varepsilon_R$.