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
ℝ, 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 xR be its real interpretation (toReal elementwise).
If:
- the target
fis approximated by a real 2-layer ReLU MLP (error ≤ εApprox), - the real MLP is close to the real interpretation of the IEEE parameters (error ≤ εQ),
- executing the IEEE MLP and then mapping to reals is close to the real interpretation of those IEEE parameters (error ≤ εR),
then the IEEE32Exec execution approximates f within εApprox + εQ + εR.