mathlib documentation

algebra.order.floor

Floor and ceil #

Summary #

We define the natural- and integer-valued floor and ceil functions on linearly ordered rings.

Main Definitions #

Notations #

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

TODO #

Some nat.floor and nat.ceil lemmas require linear_ordered_ring α. Is has_ordered_sub enough?

linear_ordered_ring/linear_ordered_semiring can be relaxed to order_ring/order_semiring in many lemmas.

Tags #

rounding, floor, ceil

Floor semiring #

@[class]
structure floor_semiring (α : Type u_2) [ordered_semiring α] :
Type u_2

A floor_semiring is a linear ordered semiring over α with a function floor : α → ℕ satisfying ∀ (n : ℕ) (x : α), n ≤ ⌊x⌋ ↔ (n : α) ≤ x).

Instances
@[protected, instance]
Equations
def nat.floor {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] :
α →

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

Equations
def nat.ceil {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] :
α →

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

Equations
theorem nat.le_floor_iff {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (ha : 0 a) :
theorem nat.le_floor {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (h : n a) :
theorem nat.floor_lt {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (ha : 0 a) :
theorem nat.lt_of_floor_lt {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (h : a⌋₊ < n) :
a < n
theorem nat.floor_le {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : 0 a) :
theorem nat.lt_succ_floor {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
theorem nat.lt_floor_add_one {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
@[simp]
theorem nat.floor_coe {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (n : ) :
@[simp]
theorem nat.floor_zero {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] :
@[simp]
theorem nat.floor_one {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] :
theorem nat.floor_of_nonpos {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} (ha : a 0) :
theorem nat.le_floor_iff' {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (hn : n 0) :
theorem nat.floor_lt' {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (hn : n 0) :
theorem nat.floor_pos {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
theorem nat.pos_of_floor_pos {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} (h : 0 < a⌋₊) :
0 < a
theorem nat.lt_of_lt_floor {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (h : n < a⌋₊) :
n < a
@[simp]
theorem nat.floor_eq_zero {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
a⌋₊ = 0 a < 1
theorem nat.floor_eq_iff {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (ha : 0 a) :
a⌋₊ = n n a a < n + 1
theorem nat.floor_eq_iff' {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (hn : n 0) :
a⌋₊ = n n a a < n + 1
theorem nat.floor_eq_on_Ico {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (n : ) (a : α) (H : a set.Ico n (n + 1)) :
theorem nat.floor_eq_on_Ico' {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (n : ) (a : α) (H : a set.Ico n (n + 1)) :
@[simp]
theorem nat.preimage_floor_of_ne_zero {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {n : } (hn : n 0) :

Ceil #

@[simp]
theorem nat.ceil_le {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } :
theorem nat.lt_ceil {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } :
theorem nat.le_ceil {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
@[simp]
theorem nat.ceil_coe {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (n : ) :
@[simp]
theorem nat.ceil_zero {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] :
@[simp]
theorem nat.ceil_eq_zero {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} :
theorem nat.lt_of_ceil_lt {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (h : a⌉₊ < n) :
a < n
theorem nat.le_of_ceil_le {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (h : a⌉₊ n) :
a n
theorem nat.floor_le_ceil {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] (a : α) :
theorem nat.floor_lt_ceil_of_lt_of_pos {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a b : α} (h : a < b) (h' : 0 < b) :
theorem nat.ceil_eq_iff {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {a : α} {n : } (hn : n 0) :
a⌉₊ = n (n - 1) < a a n
@[simp]
theorem nat.preimage_ceil_of_ne_zero {α : Type u_1} [linear_ordered_semiring α] [floor_semiring α] {n : } (hn : n 0) :
theorem nat.floor_add_nat {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] {a : α} (ha : 0 a) (n : ) :
theorem nat.floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] {a : α} (ha : 0 a) :
theorem nat.floor_sub_nat {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] (a : α) (n : ) :
theorem nat.sub_one_lt_floor {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] (a : α) :
theorem nat.ceil_add_nat {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] {a : α} (ha : 0 a) (n : ) :
theorem nat.ceil_add_one {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] {a : α} (ha : 0 a) :
theorem nat.ceil_lt_add_one {α : Type u_1} [linear_ordered_ring α] [floor_semiring α] {a : α} (ha : 0 a) :
theorem nat.floor_div_nat {α : Type u_1} [linear_ordered_field α] [floor_semiring α] (a : α) (n : ) :
theorem nat.floor_div_eq_div {α : Type u_1} [linear_ordered_field α] [floor_semiring α] (m n : ) :

Natural division is the floor of field division.

There exists at most one floor_semiring structure on a linear ordered semiring.

Floor rings #

@[class]
structure floor_ring (α : Type u_2) [linear_ordered_ring α] :
Type u_2

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

Instances
@[protected, instance]
Equations
def floor_ring.of_floor (α : Type u_1) [linear_ordered_ring α] (floor : α → ) (gc_coe_floor : galois_connection coe floor) :

A floor_ring constructor from the floor function alone.

Equations
def floor_ring.of_ceil (α : Type u_1) [linear_ordered_ring α] (ceil : α → ) (gc_ceil_coe : galois_connection ceil coe) :

A floor_ring constructor from the ceil function alone.

Equations
def int.floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
α →

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

Equations
def int.ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
α →

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

Equations
def int.fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
α

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

Equations

Floor #

theorem int.le_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {a : α} :
theorem int.floor_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {a : α} :
a < z a < z
theorem int.floor_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.floor_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 a 0 a
theorem int.floor_nonpos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : a 0) :
theorem int.lt_succ_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.lt_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.sub_one_lt_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.floor_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) :
@[simp]
theorem int.floor_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
@[simp]
theorem int.floor_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem int.floor_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem int.floor_pos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < a 1 a
@[simp]
theorem int.floor_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ) :
theorem int.floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
a + 1 = a + 1
@[simp]
theorem int.floor_int_add {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) (a : α) :
@[simp]
theorem int.floor_add_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ) :
@[simp]
theorem int.floor_nat_add {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (a : α) :
@[simp]
theorem int.floor_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ) :
@[simp]
theorem int.floor_sub_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (n : ) :
theorem int.abs_sub_lt_one_of_floor_eq_floor {α : Type u_1} [linear_ordered_comm_ring α] [floor_ring α] {a b : α} (h : a = b) :
|a - b| < 1
theorem int.floor_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {a : α} :
a = z z a a < z + 1
theorem int.floor_eq_on_Ico {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (a : α) (H : a set.Ico n (n + 1)) :
theorem int.floor_eq_on_Ico' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (n : ) (a : α) (H : a set.Ico n (n + 1)) :
@[simp]
theorem int.preimage_floor_singleton {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (m : ) :

Fractional part #

@[simp]
theorem int.self_sub_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.floor_add_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.fract_add_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.fract_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (m : ) :
@[simp]
theorem int.fract_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (m : ) :
@[simp]
theorem int.fract_int_add {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (m : ) (a : α) :
@[simp]
theorem int.self_sub_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.fract_sub_self {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.fract_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.fract_lt_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.fract_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
@[simp]
theorem int.fract_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) :
@[simp]
theorem int.fract_floor {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.floor_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.fract_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} :
int.fract a = b 0 b b < 1 ∃ (z : ), a - b = z
theorem int.fract_eq_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} :
int.fract a = int.fract b ∃ (z : ), a - b = z
@[simp]
theorem int.fract_eq_self {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
int.fract a = a 0 a a < 1
@[simp]
theorem int.fract_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.fract_add {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a b : α) :
∃ (z : ), int.fract (a + b) - int.fract a - int.fract b = z
theorem int.fract_mul_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (b : ) :
∃ (z : ), (int.fract a) * b - int.fract (a * b) = z
theorem int.preimage_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (s : set α) :
int.fract ⁻¹' s = ⋃ (m : ), (λ (x : α), x - m) ⁻¹' (s set.Ico 0 1)
theorem int.image_fract {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (s : set α) :
int.fract '' s = ⋃ (m : ), (λ (x : α), x - m) '' s set.Ico 0 1

Ceil #

theorem int.ceil_le {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {a : α} :
theorem int.floor_neg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
theorem int.ceil_neg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
theorem int.lt_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {a : α} :
z < a z < a
theorem int.ceil_le_floor_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.le_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
@[simp]
theorem int.ceil_coe {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) :
theorem int.ceil_mono {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
@[simp]
theorem int.ceil_add_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ) :
@[simp]
theorem int.ceil_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
a + 1 = a + 1
@[simp]
theorem int.ceil_sub_int {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) (z : ) :
@[simp]
theorem int.ceil_sub_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
a - 1 = a - 1
theorem int.ceil_lt_add_one {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.ceil_pos {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
0 < a 0 < a
@[simp]
theorem int.ceil_zero {α : Type u_1} [linear_ordered_ring α] [floor_ring α] :
theorem int.ceil_nonneg {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} (ha : 0 a) :
theorem int.ceil_eq_iff {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {z : } {a : α} :
a = z z - 1 < a a z
theorem int.ceil_eq_on_Ioc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) (a : α) (H : a set.Ioc (z - 1) z) :
theorem int.ceil_eq_on_Ioc' {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (z : ) (a : α) (H : a set.Ioc (z - 1) z) :
theorem int.floor_le_ceil {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.floor_lt_ceil_of_lt {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} (h : a < b) :
@[simp]
theorem int.preimage_ceil_singleton {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (m : ) :

A floor ring as a floor semiring #

@[protected, instance]
Equations
theorem int.floor_to_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :
theorem int.ceil_to_nat {α : Type u_1} [linear_ordered_ring α] [floor_ring α] (a : α) :

Intervals #

@[simp]
theorem int.preimage_Ioo {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Ico {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Ioc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Icc {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a b : α} :
@[simp]
theorem int.preimage_Ioi {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
@[simp]
theorem int.preimage_Ici {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
@[simp]
theorem int.preimage_Iio {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :
@[simp]
theorem int.preimage_Iic {α : Type u_1} [linear_ordered_ring α] [floor_ring α] {a : α} :

There exists at most one floor_ring structure on a given linear ordered ring.