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 intentionally lightweight 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

  abs.

• rel : NNReal

  rel.

• slack : NNReal

  slack.

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|

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

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

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₂

@[simp]

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

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

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₂))

@[simp]

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

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

Notation

Use open scoped ApproxTol to enable:

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

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