Floating point floor, producing Int64 or ℕ

@[irreducible]

def Floating.floor (x : Floating) : Fixed 0

Floor

Equations

• x.floor = bif x == nan || decide (2 ^ 63 < x.s) then nan else { n := x.n.shiftRightRound (2 ^ 63 - x.s) false }

theorem Floating.approx_floor (x : Floating) : approx x.floor ↑⌊x.val⌋

floor is conservative

@[simp]

theorem Floating.floor_nan : nan.floor = nan

@[simp]

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

theorem Floating.floor_mono {x y : Floating} (le : x ≤ y) (yn : y.floor ≠ nan) : x.floor ≤ y.floor

natFloor producing ℕ

def Floating.natFloor (x : Floating) : ℕ

The greatest natural definitely ≤ x (or 0 if that fails)

Equations

• x.natFloor = x.floor.n.natFloor

@[simp]

theorem Floating.natFloor_nan : nan.natFloor = 0

theorem Floating.natFloor_le {a : ℝ} {x : Floating} (ax : approx x a) : x.natFloor ≤ ⌊a⌋₊