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 (DataParallel.SyncBf16), with the standard model |rndP p x − x| ≤ 2⁻¹⁻ᵖ·|x| proved, and its commuting with scaling by 2^z (rndP_zpow_mul, which the bf16 divisor step uses). 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. Ties go toward +∞ (Mathlib's round); IEEE's ties-to-even differs only at ties, where the error bound is the same. Overflow and subnormals are idealized away, as in the standard model.

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.

    source
    theorem Proofs.int_log_zpow_mul {b : ℕ} (hb : 1 < b) (z : ℤ) {r : ℝ} (hr : 0 < r) :
    Int.log b (↑b ^ z * r) = z + Int.log b r

    Int.log b shifts by z under scaling by b^z, for any base b > 1 and any integer exponent.

    source
    theorem Proofs.int_log_abs_zpow_mul {b : ℕ} (hb : 1 < b) (z : ℤ) {x : ℝ} (hx : x ≠ 0) :
    Int.log b |↑b ^ z * x| = z + Int.log b |x|

    Int.log reads |x|, so the shift holds for either sign.

    source
    theorem Proofs.rndP_zpow_mul (p : ℕ) (z : ℤ) (x : ℝ) :
    rndP p (2 ^ z * x) = 2 ^ z * rndP p x

    The repo's rounding model commutes with scaling by a power of two — the grid at 2^z·x is the grid at x scaled by 2^z, because the exponent is unbounded. The exponent z is an integer, so this covers the multiplier R = 2^k and the divisor 1/R = 2^(-k) alike.