Tolerance

Approximation tolerances (absolute + relative).

This file defines a small, reusable tolerance object for "close enough" reasoning:

• absolute tolerance (units of the quantity),
• relative tolerance (dimensionless), and
• a nonnegative slack factor to scale the budget.

It is small and explicit and independent of any specific backend (IBP/FP32/etc.).

PyTorch correspondence / citations

PyTorch (and NumPy) commonly expose absolute + relative tolerances (often called atol/rtol) in APIs like torch.allclose / torch.testing.assert_allclose. Our approxBound follows the same pattern, but uses max |x| |y| as the relative scale so the bound is symmetric in x and y. https://pytorch.org/docs/stable/generated/torch.allclose.html https://pytorch.org/docs/stable/testing.html

structure Proofs.RuntimeApprox.ApproxTol : Type

Absolute/relative tolerance with an extra nonnegative slack factor.

• abs : NNReal

  Absolute part of the bound, which is what keeps the tolerance meaningful near zero.

• rel : NNReal

  Relative part, multiplied by the maximum magnitude of the compared values.

• slack : NNReal

  Extra nonnegative headroom. Composing two tolerated steps generally produces a bound slightly worse than either, and this field absorbs that without having to widen abs or rel.

def Proofs.RuntimeApprox.ApproxTol.ofReal (abs rel slack : ℝ) : ApproxTol

Build a tolerance from reals, clamping negatives to 0 via Real.toNNReal.

def Proofs.RuntimeApprox.ApproxTol.ofReal' (abs rel : ℝ) : ApproxTol

Default slack = 1.

def Proofs.RuntimeApprox.ApproxTol.absOnly (eps : ℝ) : ApproxTol

Absolute-only tolerance (relative = 0, slack = 1).

def Proofs.RuntimeApprox.approxBound (t : ApproxTol) (x y : ℝ) : ℝ

Scalar abs+rel error budget using max |x| |y| as the scale.

def Proofs.RuntimeApprox.approxR (x y : ℝ) (t : ApproxTol) : Prop

Scalar approximation under an abs+rel tolerance.

theorem Proofs.RuntimeApprox.approxBound_inner_nonneg (t : ApproxTol) (x y : ℝ) : 0 ≤ ↑t.abs + ↑t.rel * max |x| |y|

The absolute-plus-relative part of the budget is never negative.

All three tolerance fields are NNReal, so this is really just bookkeeping, but it is needed separately from approxBound_nonneg because the slack factor is peeled off first in the monotonicity proof below.

theorem Proofs.RuntimeApprox.approxBound_nonneg (t : ApproxTol) (x y : ℝ) : 0 ≤ approxBound t x y

The full error budget is never negative, so approxR is always satisfiable at equality.

theorem Proofs.RuntimeApprox.approxBound_mono {t₁ t₂ : ApproxTol} (habs : t₁.abs ≤ t₂.abs) (hrel : t₁.rel ≤ t₂.rel) (hslack : t₁.slack ≤ t₂.slack) (x y : ℝ) : approxBound t₁ x y ≤ approxBound t₂ x y

The budget grows when any of the three tolerance fields grows.

Monotonicity in every field is what lets a composite bound be stated with one loose tolerance rather than tracking the exact tolerance each sub-proof happened to produce.

theorem Proofs.RuntimeApprox.approxR_mono {x y : ℝ} {t₁ t₂ : ApproxTol} (habs : t₁.abs ≤ t₂.abs) (hrel : t₁.rel ≤ t₂.rel) (hslack : t₁.slack ≤ t₂.slack) (h : approxR x y t₁) : approxR x y t₂

Approximation is preserved when the tolerance is weakened.

@[simp]

theorem Proofs.RuntimeApprox.approxBound_absOnly (eps x y : ℝ) : approxBound (ApproxTol.absOnly eps) x y = ↑eps.toNNReal

With no relative term the budget is the constant eps, independent of the compared values.

theorem Proofs.RuntimeApprox.approxR_absOnly_iff {x y eps : ℝ} (heps : 0 ≤ eps) : approxR x y (ApproxTol.absOnly eps) ↔ |y - x| ≤ eps

For a nonnegative eps, absolute-only approximation is plain |y - x| ≤ eps.

The nonnegativity hypothesis is not decoration: ApproxTol stores Real.toNNReal eps, which clamps a negative input to zero, and the clamped statement would be strictly stronger than intended.

theorem Proofs.RuntimeApprox.approxR_absOnly_trans {x y z eps₁ eps₂ : ℝ} (h₁ : 0 ≤ eps₁) (h₂ : 0 ≤ eps₂) (hxy : approxR x y (ApproxTol.absOnly eps₁)) (hyz : approxR y z (ApproxTol.absOnly eps₂)) : approxR x z (ApproxTol.absOnly (eps₁ + eps₂))

Absolute errors add along a chain, by the triangle inequality.

This is the shape of every end-to-end runtime bound in this directory: each layer contributes its own eps, and the network's error is the sum. There is no analogous clean rule for the relative term, which is why the composition lemmas stay absolute-only.

@[simp]

theorem Proofs.RuntimeApprox.approxR_refl (x : ℝ) (t : ApproxTol) : approxR x x t

Every value approximates itself, at any tolerance.

theorem Proofs.RuntimeApprox.approxR_symm (x y : ℝ) (t : ApproxTol) : approxR x y t ↔ approxR y x t

The relation is symmetric, because the scale is max |x| |y| rather than |x|.

That choice is deliberate. Scaling by one argument only would make the relation asymmetric and would force every proof to fix which side is the reference value.

Notation

Use open scoped ApproxTol to enable:

x ≈[t] y meaning: approxR x y t.

def ApproxTol.«term_≈[_]_» : Lean.TrailingParserDescr