ScaleApprox #
Scale-aware approximation helpers.
This module adds an optional layer that tracks a per-tensor "scale bound" (a nonnegative bound
on linfNorm) alongside the existing eps error bounds.
It is designed to be used to derive readable abs+rel tolerances from existing eps-style proofs:
given an error budget eps and a scale bound B, we can form an ApproxTol whose rel component
is computed from (eps / B) (with safe handling of B = 0).
Nothing here changes existing forward/backward frameworks; it only provides new predicates and lemmas you can opt into.
PyTorch correspondence / citations #
This is the proof-oriented analogue of reasoning with a magnitude/scale estimate (e.g. ‖x‖∞ ≤ B)
to turn an absolute error budget into an rtol-style relative tolerance.
https://pytorch.org/docs/stable/generated/torch.allclose.html
Nonnegative scale bounds aligned with a context shape list.
- nil : BList []
- cons {s : Spec.Shape} {ss : List Spec.Shape} : NNReal → BList ss → BList (s :: ss)
Instances For
Transport a BList along an equality of the underlying shape lists.
Instances For
Transporting along rfl is the identity.
Append one additional scale bound at the end of a BList.
Instances For
Split a BList (ss ++ [τ]) into its prefix and the last bound.
Instances For
Graph evaluation appends one bound per node, so the pair snoc/unsnoc is how a scale list follows
a growing context. This lemma is what keeps the induction on graph length from having to reason
about
list append at all.
A scale bound says both spec and runtime (mapped to spec) norms are bounded by B.
Instances For
Default scale predicate on tensors (uses linfNorm).
Instances For
Context-level scale predicate aligned with a BList.
Instances For
The context scale predicate survives transporting all three arguments along the same equality.
Appending a tensor with a known scale bound extends the context predicate.
This is the step used every time a node's output is pushed onto the context: the existing bounds are untouched and the new one only has to hold for the new entry.
Conversely, a predicate on an extended context splits into the prefix part and the last entry.
Every individual entry of a context that satisfies scaleCtx satisfies its own scale bound.
Stated for an arbitrary index rather than only for the head, because a node reads its inputs from anywhere in the context.
A derived tolerance from an absolute error eps and a scale bound B.
We always keep the absolute component (abs = eps) for safety. The relative component is
computed as eps / B (with a B = 0 guard) and then clamped to be nonnegative via toNNReal
inside ApproxTol.ofReal.
Instances For
tolFromEpsScale is at least as permissive as the absolute-only tolerance in every field.
That is the whole reason the absolute component is kept rather than traded for the relative one: the
derived tolerance can then be reached from an absolute bound by monotonicity alone, with no case
analysis on whether B is zero.
An absolute tensor bound upgrades to the abs-plus-rel tolerance derived from a scale bound.
Per-entry form of the upgrade: each context slot gets the tolerance derived from its own eps
and its own scale bound.
The scale hypothesis is currently unused in the proof, since the derived tolerance is reached purely by weakening. It stays in the signature because it is what makes the resulting relative component meaningful, and dropping it would let callers form tolerances against a scale nothing satisfies.