# 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 #

source
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 `↑ : ℕ → α`.

Instances

source
instance instFloorSemiringNat :
FloorSemiring ℕ
Equations

- instFloorSemiringNat = { floor := id, ceil := id, floor_of_neg := @instFloorSemiringNat._proof_1, gc_floor := @instFloorSemiringNat._proof_2, gc_ceil := instFloorSemiringNat._proof_3 }

source
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`.

Equations

- Nat.floor = FloorSemiring.floor

Instances For

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

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

Equations

- Nat.ceil = FloorSemiring.ceil

Instances For

source
@[simp]
theorem Nat.floor_nat :
floor = id
source
@[simp]
theorem Nat.ceil_nat :
ceil = id
source
def Nat.«term⌊_⌋₊» :
Lean.ParserDescr

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

Equations

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

Instances For

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

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

Equations

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

Instances For

source
theorem Nat.le_floor_iff {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) :
n ≤ ⌊a⌋₊ ↔ ↑n ≤ a
source
theorem Nat.le_floor {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : ℕ} [IsOrderedRing α] (h : ↑n ≤ a) :
n ≤ ⌊a⌋₊
source
theorem Nat.gc_ceil_coe {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] :
GaloisConnection ceil Nat.cast
source
@[simp]
theorem Nat.ceil_le {α : Type u_2} [Semiring α] [PartialOrder α] [FloorSemiring α] {a : α} {n : ℕ} :
⌈a⌉₊ ≤ n ↔ a ≤ ↑n
source
theorem Nat.lt_ceil {α : Type u_2} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} {n : ℕ} :
n < ⌈a⌉₊ ↔ ↑n < a
source
@[simp]
theorem Nat.ceil_pos {α : Type u_2} [Semiring α] [LinearOrder α] [FloorSemiring α] {a : α} :
0 < ⌈a⌉₊ ↔ 0 < a

### Floor rings #

source
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 `↑ : ℤ → α`.

Instances

source
instance instFloorRingInt :
FloorRing ℤ
Equations

- instFloorRingInt = { floor := id, ceil := id, gc_coe_floor := instFloorRingInt._proof_1, gc_ceil_coe := instFloorRingInt._proof_2 }

source
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.

Equations

- FloorRing.ofFloor α floor gc_coe_floor = { floor := floor, ceil := fun (a : α) => -floor (-a), gc_coe_floor := gc_coe_floor, gc_ceil_coe := ⋯ }

Instances For

source
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.

Equations

- FloorRing.ofCeil α ceil gc_ceil_coe = { floor := fun (a : α) => -ceil (-a), ceil := ceil, gc_coe_floor := ⋯, gc_ceil_coe := gc_ceil_coe }

Instances For

source
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⌋`.

Equations

- Int.floor = FloorRing.floor

Instances For

source
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⌉`.

Equations

- Int.ceil = FloorRing.ceil

Instances For

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

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

Equations

- Int.fract a = a - ↑⌊a⌋

Instances For

source
@[simp]
theorem Int.floor_int :
floor = id
source
@[simp]
theorem Int.ceil_int :
ceil = id
source
@[simp]
theorem Int.fract_int :
fract = 0
source
def Int.«term⌊_⌋» :
Lean.ParserDescr

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

Equations

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

Instances For

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

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

Equations

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

Instances For

source
@[simp]
theorem Int.floorRing_floor_eq :
@FloorRing.floor = @floor
source
@[simp]
theorem Int.floorRing_ceil_eq :
@FloorRing.ceil = @ceil

#### Floor #

source
theorem Int.gc_coe_floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] :
GaloisConnection Int.cast floor
source
theorem Int.le_floor {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} :
z ≤ ⌊a⌋ ↔ ↑z ≤ a
source
theorem Int.floor_lt {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} :
⌊a⌋ < z ↔ a < ↑z
source
theorem Int.floor_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) :
↑⌊a⌋ ≤ a
source
theorem Int.floor_nonneg {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} :
0 ≤ ⌊a⌋ ↔ 0 ≤ a
source
theorem Int.floor_nonpos {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} [IsStrictOrderedRing α] (ha : a ≤ 0) :
⌊a⌋ ≤ 0

#### Ceil #

source
theorem Int.gc_ceil_coe {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] :
GaloisConnection ceil Int.cast
source
theorem Int.ceil_le {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} :
⌈a⌉ ≤ z ↔ a ≤ ↑z
source
theorem Int.lt_ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {z : ℤ} {a : α} :
z < ⌈a⌉ ↔ ↑z < a
source
theorem Int.le_ceil {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] (a : α) :
a ≤ ↑⌈a⌉
source
theorem Int.ceil_nonneg {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} [IsStrictOrderedRing α] (ha : 0 ≤ a) :
0 ≤ ⌈a⌉
source
@[simp]
theorem Int.ceil_pos {α : Type u_2} [Ring α] [LinearOrder α] [FloorRing α] {a : α} :
0 < ⌈a⌉ ↔ 0 < a

#### A floor ring as a floor semiring #

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

- FloorRing.toFloorSemiring = { floor := fun (a : α) => ⌊a⌋.toNat, ceil := fun (a : α) => ⌈a⌉.toNat, floor_of_neg := ⋯, gc_floor := ⋯, gc_ceil := ⋯ }

source
theorem Int.floor_toNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) :
⌊a⌋.toNat = ⌊a⌋₊
source
theorem Int.ceil_toNat {α : Type u_2} [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (a : α) :
⌈a⌉.toNat = ⌈a⌉₊
source
@[simp]
theorem Nat.floor_int :
floor = Int.toNat
source
@[simp]
theorem Nat.ceil_int :
ceil = Int.toNat