NF Scalar Primitive Bounds #
Scalar bridge lemmas and forward-error bounds for rounded NF primitives. These are the facts
that later tensor proofs lift pointwise across shapes.
Interpret a runtime NF scalar as a spec scalar (ℝ) by forgetting rounding metadata.
Instances For
NF → ℝ bridge lemmas #
Most approximation statements in this file are phrased over the spec scalar ℝ, but the runtime
backend is NF β fexp rnd. The following lemmas are small bridge facts that let us rewrite
runtime expressions into:
- an exact real expression in terms of
toSpec, plus - an explicit rounding operator
roundRapplied at the outermost step.
Keeping these as named lemmas (instead of repeating huge simp [...] lists) makes the later
forward-approx proofs much easier to read.
toSpec of runtime 0 is the spec scalar 0.
toSpec respects runtime exp, up to an explicit rounding step.
Forward approximation bound for sqrt (max · 0) under a positive lower bound.
This is a clamped sqrt bound: we work with sqrt (max x 0) to avoid the sqrt domain issue, but
still require a strict lower bound η > 0 on max x 0 to control conditioning via
|√a - √b| ≤ |a-b| / √η.
Forward approximation bound for addition in NF.
In words: if xR approximates x within epsx and yR approximates y within epsy,
then xR + yR approximates x + y within epsx + epsy + ulp(toSpec xR + toSpec yR)/2.
Forward approximation bound for subtraction in NF.
This is proved by reducing subtraction to addition with a negation and applying approx_add_nf.
Forward approximation bound for negation in NF (rounding error on -toSpec xR).
Forward approximation bound for absolute value in NF (abs is pure + a final rounding).
Forward approximation bound for exp in NF.
Uses the mean value theorem for Real.exp to bound the propagation of input error, then adds one
rounding-ULP term for the final NF rounding.
Forward approximation bound for tanh in NF (coarse but unconditional).
Because tanh is bounded in [-1, 1], we always have |tanh(toSpec xR) - tanh(x)| ≤ 2, and then
we add one rounding-ULP term for the final NF rounding step.
Clamped log on spec scalars: log (max x ε).
This is used to obtain unconditional forward bounds for log by avoiding the singularity at 0.
Instances For
Clamped log on runtime NF scalars (implemented as NF.ofReal (safeLog (toSpec xR))).
This definition keeps the semantic spec function explicit (so proofs can reason about it) while still producing an executable runtime scalar.
Instances For
Forward approximation bound for safeLog in NF.
On the clamped domain u,v ≥ ε > 0, log is (1/ε)-Lipschitz. We use that to propagate the input
error and then add one rounding-ULP term for the final NF rounding.
Forward approximation bound for multiplication in NF.
This has the standard "first-order" shape:
terms proportional to |toSpec xR| * epsy and |toSpec yR| * epsx, plus an ulp term for the
final
rounding. (For classical background, see Higham, Accuracy and Stability of Numerical Algorithms.)
Forward approximation bound for division under a coarse denominator lower bound (y ≥ 1).
Division is ill-conditioned near 0, so we need a domain condition. This lemma is tailored for the
simple case y ≥ 1 to keep constants small.
Forward approximation bound for division under a general positive lower bound (η ≤ y with η > 0).
This is the more general variant of approx_div_nf_of_one_le, making the conditioning explicit via
the factor (1/η).
Forward approximation bound for scaling (elementwise multiply by a runtime constant c).