Floor and ceil

We define the natural- and integer-valued floor and ceil functions on linearly ordered rings. We also provide positivity extensions to handle floor and ceil.

Main definitions

• FloorSemiring: An ordered semiring with natural-valued floor and ceil.

• Nat.floor a: Greatest natural n such that n ≤ a. Equal to 0 if a < 0.

• Nat.ceil a: Least natural n such that a ≤ n.

• FloorRing: A linearly ordered ring with integer-valued floor and ceil.

• Int.floor a: Greatest integer z such that z ≤ a.

• Int.ceil a: Least integer z such that a ≤ z.

• Int.fract a: Fractional part of a, defined as a - floor a.

Notation

• ⌊a⌋₊ is Nat.floor a.
• ⌈a⌉₊ is Nat.ceil a.
• ⌊a⌋ is Int.floor a.
• ⌈a⌉ is Int.ceil a.

The index ₊ in the notations for Nat.floor and Nat.ceil is used in analogy to the notation for nnnorm.

TODO

LinearOrderedRing/LinearOrderedSemiring can be relaxed to OrderedRing/OrderedSemiring in many lemmas.

Tags

rounding, floor, ceil

Floor semiring

class FloorSemiring (α : Type u_4) [Semiring α] [PartialOrder α] : Type u_4

A FloorSemiring is an ordered semiring over α with a function floor : α → ℕ satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x). Note that many lemmas require a LinearOrder. Please see the above TODO.

• floor : α → ℕ

  FloorSemiring.floor a computes the greatest natural n such that (n : α) ≤ a.

• ceil : α → ℕ

  FloorSemiring.ceil a computes the least natural n such that a ≤ (n : α).

• floor_of_neg {a : α} (ha : a < 0) : floor a = 0

  FloorSemiring.floor of a negative element is zero.

• gc_floor {a : α} {n : ℕ} (ha : 0 ≤ a) : n ≤ floor a ↔ ↑n ≤ a

  A natural number n is smaller than FloorSemiring.floor a iff its coercion to α is smaller than a.

• gc_ceil : GaloisConnection ceil Nat.cast

  FloorSemiring.ceil is the lower adjoint of the coercion ↑ : ℕ → α.

instance instFloorSemiringNat : FloorSemiring ℕ

def Nat.floor {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] : α → ℕ

⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

def Nat.ceil {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] : α → ℕ

⌈a⌉₊ is the least natural n such that a ≤ n

@[simp]

theorem Nat.floor_nat : floor = id

@[simp]

theorem Nat.ceil_nat : ceil = id

def Nat.«term⌊_⌋₊» : Lean.ParserDescr

⌊a⌋₊ is the greatest natural n such that n ≤ a. If a is negative, then ⌊a⌋₊ = 0.

def Nat.«term⌈_⌉₊» : Lean.ParserDescr

⌈a⌉₊ is the least natural n such that a ≤ n

theorem Nat.le_floor_iff {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) : n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

theorem Nat.le_floor {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : ℕ} [IsOrderedRing α] (h : ↑n ≤ a) : n ≤ ⌊a⌋₊

theorem Nat.gc_ceil_coe {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] : GaloisConnection ceil Nat.cast

@[simp]

theorem Nat.ceil_le {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : ℕ} : ⌈a⌉₊ ≤ n ↔ a ≤ ↑n

theorem Nat.lt_ceil {α : Type u_2} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} {n : ℕ} : n < ⌈a⌉₊ ↔ ↑n < a

@[simp]

theorem Nat.ceil_pos {α : Type u_2} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} : 0 < ⌈a⌉₊ ↔ 0 < a

Floor rings

class FloorRing (α : Type u_4) [Ring α] [LinearOrder α] : Type u_4

A FloorRing is a linear ordered ring over α with a function floor : α → ℤ satisfying ∀ (z : ℤ) (a : α), z ≤ floor a ↔ (z : α) ≤ a).

• floor : α → ℤ

  FloorRing.floor a computes the greatest integer z such that (z : α) ≤ a.

• ceil : α → ℤ

  FloorRing.ceil a computes the least integer z such that a ≤ (z : α).

• gc_coe_floor : GaloisConnection Int.cast floor

  FloorRing.ceil is the upper adjoint of the coercion ↑ : ℤ → α.

• gc_ceil_coe : GaloisConnection ceil Int.cast

  FloorRing.ceil is the lower adjoint of the coercion ↑ : ℤ → α.

instance instFloorRingInt : FloorRing ℤ

def FloorRing.ofFloor (α : Type u_4) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (floor : α → ℤ) (gc_coe_floor : GaloisConnection Int.cast floor) : FloorRing α

A FloorRing constructor from the floor function alone.

def FloorRing.ofCeil (α : Type u_4) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (ceil : α → ℤ) (gc_ceil_coe : GaloisConnection ceil Int.cast) : FloorRing α

A FloorRing constructor from the ceil function alone.

theorem exists_floor' {α : Type u_4} [Ring α] [PartialOrder α] [IsStrictOrderedRing α] (x : α) (below : ∃ (n : ℤ), ↑n ≤ x) (above : ∃ (n : ℤ), x ≤ ↑n) : ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

See exists_floor for a variant which instead assumes an Archimedean ring.

noncomputable def FloorRing.ofBounded (α : Type u_4) [Ring α] [LinearOrder α] [IsStrictOrderedRing α] (bounded : ∀ (x : α), ∃ (n : ℕ), x ≤ ↑n) : FloorRing α

Construct a FloorRing instance noncomputably, from the hypothesis that every element is bounded above by a natural number.

def Int.floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] : α → ℤ

Int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

def Int.ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] : α → ℤ

Int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

def Int.fract {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) : α

Int.fract a the fractional part of a, is a minus its floor.

@[simp]

theorem Int.floor_int : floor = id

@[simp]

theorem Int.ceil_int : ceil = id

@[simp]

theorem Int.fract_int : fract = 0

def Int.«term⌊_⌋» : Lean.ParserDescr

Int.floor a is the greatest integer z such that z ≤ a. It is denoted with ⌊a⌋.

def Int.«term⌈_⌉» : Lean.ParserDescr

Int.ceil a is the smallest integer z such that a ≤ z. It is denoted with ⌈a⌉.

@[simp]

theorem Int.floorRing_floor_eq : @FloorRing.floor = @floor

@[simp]

theorem Int.floorRing_ceil_eq : @FloorRing.ceil = @ceil

Floor

theorem Int.gc_coe_floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] : GaloisConnection Int.cast floor

theorem Int.le_floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} : z ≤ ⌊a⌋ ↔ ↑z ≤ a

theorem Int.floor_lt {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} : ⌊a⌋ < z ↔ a < ↑z

theorem Int.floor_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) : ↑⌊a⌋ ≤ a

theorem Int.floor_nonneg {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} : 0 ≤ ⌊a⌋ ↔ 0 ≤ a

theorem Int.floor_nonpos {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} [IsStrictOrderedRing α] (ha : a ≤ 0) : ⌊a⌋ ≤ 0

Ceil

theorem Int.gc_ceil_coe {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] : GaloisConnection ceil Int.cast

theorem Int.ceil_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} : ⌈a⌉ ≤ z ↔ a ≤ ↑z

theorem Int.lt_ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} : z < ⌈a⌉ ↔ ↑z < a

theorem Int.le_ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) : a ≤ ↑⌈a⌉

theorem Int.ceil_nonneg {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} [IsStrictOrderedRing α] (ha : 0 ≤ a) : 0 ≤ ⌈a⌉

@[simp]

theorem Int.ceil_pos {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} : 0 < ⌈a⌉ ↔ 0 < a

A floor ring as a floor semiring

@[instance 100]

instance FloorRing.toFloorSemiring {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] : FloorSemiring α

theorem Int.floor_toNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) : ⌊a⌋.toNat = ⌊a⌋₊

theorem Int.ceil_toNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) : ⌈a⌉.toNat = ⌈a⌉₊

@[simp]

theorem Nat.floor_int : floor = Int.toNat

@[simp]

theorem Nat.ceil_int : ceil = Int.toNat