Rounding Predicates

Semantic specifications for directed, toward-zero, and nearest rounding. They are independent of any radix or concrete format: a predicate F : ℝ → Prop identifies the representable values, and the point predicates characterize the required output among those values.

These definitions correspond to Flocq's Rnd_DN_pt, Rnd_UP_pt, Rnd_ZR_pt, and Rnd_N_pt.

def FloatLib.Floats.Formats.Flocq.RoundDownPoint (F : ℝ → Prop) (x f : ℝ) : Prop

f is the greatest F-value no larger than x.

def FloatLib.Floats.Formats.Flocq.RoundUpPoint (F : ℝ → Prop) (x f : ℝ) : Prop

f is the least F-value no smaller than x.

theorem FloatLib.Floats.Formats.Flocq.roundDownPoint_iff_isGreatest (F : ℝ → Prop) (x f : ℝ) : RoundDownPoint F x f ↔ IsGreatest {g : ℝ | F g ∧ g ≤ x} f

A downward rounding point is a greatest element of the representable lower bounds.

theorem FloatLib.Floats.Formats.Flocq.roundUpPoint_iff_isLeast (F : ℝ → Prop) (x f : ℝ) : RoundUpPoint F x f ↔ IsLeast {g : ℝ | F g ∧ x ≤ g} f

An upward rounding point is a least element of the representable upper bounds.

def FloatLib.Floats.Formats.Flocq.RoundTowardZeroPoint (F : ℝ → Prop) (x f : ℝ) : Prop

Directed down on nonnegative inputs and directed up on nonpositive inputs.

def FloatLib.Floats.Formats.Flocq.RoundNearestPoint (F : ℝ → Prop) (x f : ℝ) : Prop

f is an F-value at least as close to x as every other representable value.

def FloatLib.Floats.Formats.Flocq.RoundDown (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds downward with respect to F at every input.

def FloatLib.Floats.Formats.Flocq.RoundUp (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds upward with respect to F at every input.

def FloatLib.Floats.Formats.Flocq.RoundTowardZero (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds toward zero with respect to F at every input.

def FloatLib.Floats.Formats.Flocq.RoundNearest (F : ℝ → Prop) (round : ℝ → ℝ) : Prop

A rounding function rounds to a nearest F-value at every input.

theorem FloatLib.Floats.Formats.Flocq.roundDownPoint_unique {F : ℝ → Prop} {x f g : ℝ} (hf : RoundDownPoint F x f) (hg : RoundDownPoint F x g) : f = g

A downward rounding point is unique.

theorem FloatLib.Floats.Formats.Flocq.roundUpPoint_unique {F : ℝ → Prop} {x f g : ℝ} (hf : RoundUpPoint F x f) (hg : RoundUpPoint F x g) : f = g

An upward rounding point is unique.

theorem FloatLib.Floats.Formats.Flocq.roundDownPoint_refl {F : ℝ → Prop} {x : ℝ} (hx : F x) : RoundDownPoint F x x

A representable value is its own downward rounding point.

theorem FloatLib.Floats.Formats.Flocq.roundUpPoint_refl {F : ℝ → Prop} {x : ℝ} (hx : F x) : RoundUpPoint F x x

A representable value is its own upward rounding point.

theorem FloatLib.Floats.Formats.Flocq.roundUpPoint_neg {F : ℝ → Prop} (hneg : ∀ (x : ℝ), F x → F (-x)) {x f : ℝ} (hf : RoundDownPoint F x f) : RoundUpPoint F (-x) (-f)

Negation turns a downward point into an upward point for a symmetric format.

theorem FloatLib.Floats.Formats.Flocq.roundDownPoint_neg {F : ℝ → Prop} (hneg : ∀ (x : ℝ), F x → F (-x)) {x f : ℝ} (hf : RoundUpPoint F x f) : RoundDownPoint F (-x) (-f)

Negation turns an upward point into a downward point for a symmetric format.

theorem FloatLib.Floats.Formats.Flocq.roundDownUpPoint_split {F : ℝ → Prop} {x d u f : ℝ} (hd : RoundDownPoint F x d) (hu : RoundUpPoint F x u) (hf : F f) : f ≤ d ∨ u ≤ f

Any representable value lies below the downward point or above the upward point.

theorem FloatLib.Floats.Formats.Flocq.roundNearestPoint_of_down_up {F : ℝ → Prop} {x d u f : ℝ} (hd : RoundDownPoint F x d) (hu : RoundUpPoint F x u) (hf : F f) (hfd : |f - x| ≤ |d - x|) (hfu : |f - x| ≤ |u - x|) : RoundNearestPoint F x f

A representable value no farther than both directed neighbors is globally nearest. Every other representable value lies outside the interval between those neighbors.