Successor and Predecessor

The neighboring values follow Flocq's Core/Ulp.v. At a positive radix boundary, the spacing below the value can differ from the spacing above it, so predPos uses the preceding magnitude's exponent in that case.

noncomputable def FloatLib.Floats.Formats.Flocq.predPos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : ℝ

Previous-value formula for a nonnegative input.

noncomputable def FloatLib.Floats.Formats.Flocq.succ {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : ℝ

Successor in the generic format, defined by positive spacing and sign symmetry.

noncomputable def FloatLib.Floats.Formats.Flocq.pred {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : ℝ

Predecessor, defined as the negated successor of the negated input.

theorem FloatLib.Floats.Formats.Flocq.succ_eq_of_nonneg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 ≤ x) : succ x = x + ulp β fexp x

On nonnegative inputs, successor adds one ULP.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.succ_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : succ (-x) = -pred x

Successor and predecessor are exchanged by negation.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.pred_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : pred (-x) = -succ x

Predecessor and successor are exchanged by negation.

theorem FloatLib.Floats.Formats.Flocq.succ_zero {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] : succ 0 = ulp β fexp 0

The successor of zero is the format's zero ULP.

theorem FloatLib.Floats.Formats.Flocq.pred_zero {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] : pred 0 = -ulp β fexp 0

The predecessor of zero is the negated zero ULP.

theorem FloatLib.Floats.Formats.Flocq.pred_eq_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 ≤ x) : pred x = predPos x

On nonnegative inputs, the symmetric predecessor agrees with predPos.

theorem FloatLib.Floats.Formats.Flocq.pred_bpow {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (e : ℤ) : pred (bpow β e) = bpow β e - bpow β (fexp e)

The predecessor of a radix power uses the spacing from the bin immediately below it.

theorem FloatLib.Floats.Formats.Flocq.predPos_le {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : predPos x ≤ x

The positive predecessor formula never exceeds its input.

theorem FloatLib.Floats.Formats.Flocq.predPos_lt {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : x ≠ 0) : predPos x < x

Away from zero, the positive predecessor formula is strictly smaller than its input.

theorem FloatLib.Floats.Formats.Flocq.le_succ {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : x ≤ succ x

Successor never falls below its input.

theorem FloatLib.Floats.Formats.Flocq.pred_le {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : pred x ≤ x

Predecessor never exceeds its input.

theorem FloatLib.Floats.Formats.Flocq.lt_succ {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : x ≠ 0) : x < succ x

Successor is strictly larger away from zero.

theorem FloatLib.Floats.Formats.Flocq.pred_lt {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : x ≠ 0) : pred x < x

Predecessor is strictly smaller away from zero.

theorem FloatLib.Floats.Formats.Flocq.succ_le_magnitude_bpow_of_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 < x) (hfmt : genericFormat β fexp x) : succ x ≤ bpow β (magnitude β x)

A positive representable value's successor does not exceed its magnitude boundary.

theorem FloatLib.Floats.Formats.Flocq.generic_format_succ_of_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 < x) (hfmt : genericFormat β fexp x) : genericFormat β fexp (succ x)

The successor of a positive representable value is representable.

theorem FloatLib.Floats.Formats.Flocq.generic_format_sub_ulp_of_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 < x) (hfmt : genericFormat β fexp x) (hboundary : x ≠ bpow β (magnitude β x - 1)) : genericFormat β fexp (x - ulp β fexp x)

Subtracting one ULP from a positive representable value that is not a radix boundary remains representable in the same magnitude bin.

theorem FloatLib.Floats.Formats.Flocq.generic_format_bpow_sub_prev_spacing {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (k : ℤ) (hfmt : genericFormat β fexp (bpow β k)) : genericFormat β fexp (bpow β k - bpow β (fexp k))

Subtracting the preceding-bin spacing from a representable radix power is representable.

theorem FloatLib.Floats.Formats.Flocq.generic_format_predPos_of_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hx : 0 < x) (hfmt : genericFormat β fexp x) : genericFormat β fexp (predPos x)

The predecessor formula for a positive representable input yields a representable value.

theorem FloatLib.Floats.Formats.Flocq.generic_format_succ {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hfmt : genericFormat β fexp x) : genericFormat β fexp (succ x)

The successor of every representable value is representable.

theorem FloatLib.Floats.Formats.Flocq.generic_format_pred {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x : ℝ} (hfmt : genericFormat β fexp x) : genericFormat β fexp (pred x)

The predecessor of every representable value is representable.

theorem FloatLib.Floats.Formats.Flocq.succ_le_of_lt_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] {x y : ℝ} (hx : 0 < x) (hxfmt : genericFormat β fexp x) (hyfmt : genericFormat β fexp y) (hxy : x < y) : succ x ≤ y

No representable value lies strictly between a positive grid point and its successor.