Documentation

Interval.Floating.Order

Floating point ordering #

We choose to make Floating a linear order with ∀ x, nan ≤ x, though unfortunately this means max can't propagate nan. We provide an Floating.max version which does.

@[irreducible]

def Floating.blt (x y : Floating) :

Unlike Float, we don't worry about nan for our comparisons

Equations

One or more equations did not get rendered due to their size.

Instances For

@[irreducible]

def Floating.ble (x y : Floating) :

Unlike Float, we don't worry about nan for our comparisons

Equations

x.ble y = !y.blt x

Instances For

instance Floating.instLT :

Equations

Floating.instLT = { lt := fun (x y : Floating) => x.blt y = true }

instance Floating.instLE :

Equations

Floating.instLE = { le := fun (x y : Floating) => x.ble y = true }

instance Floating.instDecidableRelLt :

DecidableRel fun (x1 x2 : Floating) => x1 < x2

Equations

x✝¹.instDecidableRelLt x✝ = id inferInstance

instance Floating.instDecidableRelLe :

DecidableRel fun (x1 x2 : Floating) => x1 ≤ x2

Equations

x✝¹.instDecidableRelLe x✝ = id inferInstance

instance Floating.instMin :

Equations

Floating.instMin = { min := fun (x y : Floating) => bif x.ble y then x else y }

instance Floating.instMax :

We define max so that Floating is a LinearOrder, though unfortunately this means that it does not propagate nan correctly. Floating.max works better.

Equations

Floating.instMax = { max := fun (x y : Floating) => bif x.ble y then y else x }

@[irreducible]

def Floating.max (x y : Floating) :

A version of max that propagates nan

Equations

x.max y = -min (-x) (-y)

Instances For

theorem Floating.blt_eq_lt {x y : Floating} :

x.blt y = decide (x < y)

Turn blt into <

theorem Floating.ble_eq_le {x y : Floating} :

x.ble y = decide (x ≤ y)

Turn ble into <

theorem Floating.min_def (x y : Floating) :

min x y = if x ≤ y then x else y

min in terms of ≤

theorem Floating.max_def (x y : Floating) :

Max.max x y = if x ≤ y then y else x

max in terms of ≤

theorem Floating.lt_def {x y : Floating} :

x < y ↔ x.n.isNeg > y.n.isNeg ∨ x.n.isNeg = y.n.isNeg ∧ ((if x.n.isNeg = true then x.s > y.s else x.s < y.s) ∨ x.s = y.s ∧ x.n.toUInt64 < y.n.toUInt64)

< in more mathematical terms

theorem Floating.le_def {x y : Floating} :

x ≤ y ↔ ¬y < x

≤ in terms of <

@[simp]

theorem Floating.neg_lt_neg {x y : Floating} (xm : x ≠ nan) (ym : y ≠ nan) :

-x < -y ↔ y < x

< respects -

@[simp]

theorem Floating.neg_le_neg {x y : Floating} (xm : x ≠ nan) (ym : y ≠ nan) :

-x ≤ -y ↔ y ≤ x

≤ respects -

@[simp]

theorem Floating.nan_lt_zero :

nan appears negative

theorem Floating.not_lt_self (x : Floating) :

¬x < x

Our ordering is antireflexive

theorem Floating.not_lt_of_lt {x y : Floating} (xy : x < y) :

¬y < x

< is antisymmetric

theorem Floating.le_antisymm' {x y : Floating} (xy : x ≤ y) (yx : y ≤ x) :

x = y

≤ is antisymmetric

theorem Floating.isNeg_iff' {x : Floating} :

x.n < 0 ↔ x < 0

x.n.isNeg determines negativity

@[simp]

theorem Floating.le_coe_coe_n {x : Floating} (s0 : x.s ≠ 0) (xn : 0 ≤ x.n) :

2 ^ 62 ≤ ↑↑x.n

Strict upper bound for ↑↑x.n, if we're normalized and positive

@[simp]

theorem Floating.coe_coe_n_lt {x : Floating} :

↑↑x.n < 2 ^ 63

Strict upper bound for ↑↑x.n

@[simp]

theorem Floating.neg_coe_coe_n_lt {x : Floating} (n : x ≠ nan) :

-↑↑x.n < 2 ^ 63

Strict upper bound for -↑↑x.n

@[simp]

theorem Floating.neg_coe_coe_n_le (x : Floating) :

-↑↑x.n ≤ 2 ^ 63

Upper bound for -↑↑x.n

@[simp]

theorem Floating.nan_lt {x : Floating} (n : x ≠ nan) :

nan is the unique minimum

@[simp]

theorem Floating.nan_le (x : Floating) :

nan is the minimum

@[simp]

theorem Floating.val_nan_lt {x : Floating} (n : x ≠ nan) :

nan.val < x.val

nan is the unique minimum, val version

@[simp]

theorem Floating.val_nan_le (x : Floating) :

nan.val ≤ x.val

nan is the minimum, val version

@[simp]

theorem Floating.not_lt_nan (x : Floating) :

nan is the minimum

@[simp]

theorem Floating.not_lt_nan_val (x : Floating) :

¬x.val < nan.val

nan is the minimum

@[simp]

theorem Floating.isNeg_iff {x : Floating} :

x.n < 0 ↔ x.val < 0

x.n.isNeg determines negativity, val version

@[simp]

theorem Floating.n_nonneg_iff {x : Floating} :

0 ≤ x.n ↔ 0 ≤ x.val

0 ≤ x.n determines nonnegativity, val version

theorem Floating.val_lt_val_of_nonneg {x y : Floating} (xn : 0 ≤ x.n) (yn : 0 ≤ y.n) :

x.val < y.val ↔ x < y

The order is consistent with .val, nonnegative case

@[simp]

theorem Floating.val_lt_val {x y : Floating} :

x < y ↔ x.val < y.val

The order is consistent with .val

@[simp]

theorem Floating.val_le_val {x y : Floating} :

x ≤ y ↔ x.val ≤ y.val

The order is consistent with .val

theorem Floating.val_le_val_of_le {x y : Floating} (le : x ≤ y) :

x.val ≤ y.val

instance Floating.instLinearOrder :

LinearOrder Floating

Floating is a partial order

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Floating.val_inj {x y : Floating} :

x.val = y.val ↔ x = y

val is injective

@[simp]

theorem Floating.lt_zero_iff {x : Floating} :

x < 0 ↔ x.val < 0

@[simp]

theorem Floating.nonneg_iff {x : Floating} :

0 ≤ x ↔ 0 ≤ x.val

@[simp]

theorem Floating.not_nan_nonneg :

¬0 ≤ nan.val

@[simp]

theorem Floating.not_nan_pos :

theorem Floating.ne_nan_of_nonneg {x : Floating} (n : 0 ≤ x.val) :

theorem Floating.ne_nan_of_le {x y : Floating} (n : x ≠ nan) (le : x.val ≤ y.val) :

theorem Floating.n_lt_of_nonneg {x : Floating} (x0 : 0 ≤ x.val) :

x.n.toUInt64.toNat < 2 ^ 63

If we're positive, n is small

Facts about `min` and `max` #

@[simp]

theorem Floating.min_nan (x : Floating) :

min x nan = nan

min propagates nan

@[simp]

theorem Floating.nan_min (x : Floating) :

min nan x = nan

min propagates nan

theorem Floating.ne_nan_of_min {x y : Floating} (n : min x y ≠ nan) :

x ≠ nan ∧ y ≠ nan

min propagates nan

theorem Floating.eq_nan_of_min {x y : Floating} (n : min x y = nan) :

x = nan ∨ y = nan

min never produces new nans

@[simp]

theorem Floating.max_nan (x : Floating) :

x.max nan = nan

Floating.max propagates nan (Max.max does not)

@[simp]

theorem Floating.nan_max (x : Floating) :

nan.max x = nan

Floating.max propagates nan (Max.max does not)

theorem Floating.ne_nan_of_max {x y : Floating} (n : x.max y ≠ nan) :

x ≠ nan ∧ y ≠ nan

Floating.min propagates nan (Max.max does not)

theorem Floating.eq_nan_of_max {x y : Floating} (n : x.max y = nan) :

x = nan ∨ y = nan

Floating.max never produces new nans

@[simp]

theorem Floating.min_eq_nan {x y : Floating} :

min x y = nan ↔ x = nan ∨ y = nan

min is nan if an argument is

@[simp]

theorem Floating.max_eq_nan {x y : Floating} :

x.max y = nan ↔ x = nan ∨ y = nan

Floating.max is nan if an argument is

@[simp]

theorem Floating.max_eq_nan' {x y : Floating} :

Max.max x y = nan ↔ x = nan ∧ y = nan

max is nan if both arguments are

@[simp]

theorem Floating.max_ne_nan {x y : Floating} :

x.max y ≠ nan ↔ x ≠ nan ∧ y ≠ nan

Floating.max is nan if an argument is

@[simp]

theorem Floating.val_min {x y : Floating} :

(min x y).val = min x.val y.val

min commutes with val

@[simp]

theorem Floating.val_max {x y : Floating} (xn : x ≠ nan) (yn : y ≠ nan) :

(x.max y).val = Max.max x.val y.val

Floating.max commutes with val away from nan

@[simp]

theorem Floating.val_max' {x y : Floating} (n : x.max y ≠ nan) :

(x.max y).val = Max.max x.val y.val

Floating.max commutes with val away from nan

@[simp]

theorem Floating.max_self (x : Floating) :

x.max x = x

theorem Floating.max_comm (x y : Floating) :

x.max y = y.max x

Floating.max is commutative

theorem Floating.max_assoc (x y z : Floating) :

(x.max y).max z = x.max (y.max z)

Floating.max is associative

@[simp]

theorem Floating.max_eq_left {x y : Floating} (yx : y.val ≤ x.val) (yn : y ≠ nan) :

x.max y = x

max_eq_left for Floating.max, if we're not nan

@[simp]

theorem Floating.max_eq_right {x y : Floating} (xy : x.val ≤ y.val) (xn : x ≠ nan) :

x.max y = y

max_eq_right for Floating.max, if we're not nan

@[simp]

theorem Floating.val_nan_lt_zero :

@[simp]

theorem Floating.val_nan_le_zero :

Additional facts about "naive" min and max (discarding single nans) #

Min.min propagates nans, and Max.max is already naive, so we only need to define naive_min.

def Floating.naive_min (x y : Floating) :

min that discards single nans

Equations

x.naive_min y = -max (-x) (-y)

Instances For

theorem Floating.naive_min_eq_nan {x y : Floating} :

x.naive_min y = nan ↔ x = nan ∧ y = nan

theorem Floating.naive_max_eq_nan {x y : Floating} :

Max.max x y = nan ↔ x = nan ∧ y = nan

@[simp]

theorem Floating.nan_naive_min {x : Floating} :

nan.naive_min x = x

@[simp]

theorem Floating.naive_min_nan {x : Floating} :

x.naive_min nan = x

@[simp]

theorem Floating.nan_naive_max {x : Floating} :

Max.max nan x = x

@[simp]

theorem Floating.naive_max_nan {x : Floating} :

Max.max x nan = x

@[simp]

theorem Floating.val_naive_max {x y : Floating} :

(Max.max x y).val = Max.max x.val y.val

Max.max commutes with val

@[simp]

theorem Floating.val_naive_min {x y : Floating} (xn : x ≠ nan) (yn : y ≠ nan) :

(x.naive_min y).val = min x.val y.val

naive_min commutes with val if neither argument is nan