Documentation

LeanMlir.Proofs.Float.RndP

rndP — round-to-nearest on the unbounded-exponent p-bit grid #

The rounding operator behind the named float models (binary32, fp8E4M3 in Binary32Instance.lean) and the bf16 sharding lemmas (DataParallelSyncBf16.lean), with the standard model |rndP p x − x| ≤ 2⁻¹⁻ᵖ·|x| proved. A leaf on Mathlib alone, so a consumer that needs only the operator does not import FloatBridge.

source
noncomputable def Proofs.rndP (p : ℕ) (x : ℝ) :
ℝ

Round-to-nearest on the unbounded-exponent p-bit-significand grid. For x ≠ 0 with binade exponent e = Int.log 2 |x| (i.e. 2^e ≤ |x| < 2^(e+1)), round x to the nearest multiple of 2^(e−p) — a significand of p fractional bits, every exponent available. This is IEEE round-to-nearest minus overflow and subnormals, the standard-model idealization.

Equations
Instances For
    source
    @[simp]
    theorem Proofs.rndP_zero (p : ℕ) :
    rndP p 0 = 0
    source
    theorem Proofs.rndP_err (p : ℕ) (x : ℝ) :
    |rndP p x - x| ≤ (2 ^ (p + 1))⁻¹ * |x|

    The standard model, PROVED (formerly the ieeeRnd_err axiom): |rndP p x − x| ≤ 2⁻¹⁻ᵖ·|x|. The grid spacing at x is 2^(e−p), nearest-rounding contributes half a step 2^(e−p−1), and 2^e ≤ |x| turns that into the relative bound. Mathlib-only: Int.zpow_log_le_self + abs_sub_round.