Floor and ceil

Summary

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

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.

• round a: Nearest integer to a. It rounds halves towards infinity.

Notations

• ⌊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) [OrderedSemiring α] : 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 : α}, a < 0 → FloorSemiring.floor a = 0

  FloorSemiring.floor of a negative element is zero.

• gc_floor : ∀ {a : α} {n : ℕ}, 0 ≤ a → (n ≤ FloorSemiring.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 FloorSemiring.ceil Nat.cast

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

theorem FloorSemiring.floor_of_neg {α : Type u_4} : ∀ {inst : OrderedSemiring α} [self : FloorSemiring α] {a : α}, a < 0 → FloorSemiring.floor a = 0

FloorSemiring.floor of a negative element is zero.

theorem FloorSemiring.gc_floor {α : Type u_4} : ∀ {inst : OrderedSemiring α} [self : FloorSemiring α] {a : α} {n : ℕ}, 0 ≤ a → (n ≤ FloorSemiring.floor a ↔ ↑n ≤ a)

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

theorem FloorSemiring.gc_ceil {α : Type u_4} : ∀ {inst : OrderedSemiring α} [self : FloorSemiring α], GaloisConnection FloorSemiring.ceil Nat.cast

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

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 }

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

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

Equations

• Nat.floor = FloorSemiring.floor

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

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

Equations

• Nat.ceil = FloorSemiring.ceil

@[simp]

theorem Nat.floor_nat : Nat.floor = id

@[simp]

theorem Nat.ceil_nat : Nat.ceil = id

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

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

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

@[simp]

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

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

theorem Nat.floor_lt_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : ⌊a⌋₊ < 1 ↔ a < 1

theorem Nat.lt_of_floor_lt {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (h : ⌊a⌋₊ < n) : a < ↑n

theorem Nat.lt_one_of_floor_lt_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (h : ⌊a⌋₊ < 1) : a < 1

theorem Nat.floor_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : ↑⌊a⌋₊ ≤ a

theorem Nat.lt_succ_floor {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) : a < ↑⌊a⌋₊.succ

theorem Nat.lt_floor_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) : a < ↑⌊a⌋₊ + 1

@[simp]

theorem Nat.floor_natCast {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) : ⌊↑n⌋₊ = n

@[deprecated Nat.floor_natCast]

theorem Nat.floor_coe {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) : ⌊↑n⌋₊ = n

Alias of Nat.floor_natCast.

@[simp]

theorem Nat.floor_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : ⌊0⌋₊ = 0

@[simp]

theorem Nat.floor_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : ⌊1⌋₊ = 1

@[simp]

theorem Nat.floor_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) [n.AtLeastTwo] : ⌊OfNat.ofNat n⌋₊ = n

theorem Nat.floor_of_nonpos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : a ≤ 0) : ⌊a⌋₊ = 0

theorem Nat.floor_mono {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : Monotone Nat.floor

theorem Nat.floor_le_floor {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (hab : a ≤ b) : ⌊a⌋₊ ≤ ⌊b⌋₊

theorem Nat.le_floor_iff' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (hn : n ≠ 0) : n ≤ ⌊a⌋₊ ↔ ↑n ≤ a

@[simp]

theorem Nat.one_le_floor_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (x : α) : 1 ≤ ⌊x⌋₊ ↔ 1 ≤ x

theorem Nat.floor_lt' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (hn : n ≠ 0) : ⌊a⌋₊ < n ↔ a < ↑n

theorem Nat.floor_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} : 0 < ⌊a⌋₊ ↔ 1 ≤ a

theorem Nat.pos_of_floor_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (h : 0 < ⌊a⌋₊) : 0 < a

theorem Nat.lt_of_lt_floor {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (h : n < ⌊a⌋₊) : ↑n < a

theorem Nat.floor_le_of_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (h : a ≤ ↑n) : ⌊a⌋₊ ≤ n

theorem Nat.floor_le_one_of_le_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (h : a ≤ 1) : ⌊a⌋₊ ≤ 1

@[simp]

theorem Nat.floor_eq_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} : ⌊a⌋₊ = 0 ↔ a < 1

theorem Nat.floor_eq_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

theorem Nat.floor_eq_iff' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1

theorem Nat.floor_eq_on_Ico {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) (a : α) : a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋₊ = n

theorem Nat.floor_eq_on_Ico' {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) (a : α) : a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋₊ = ↑n

@[simp]

theorem Nat.preimage_floor_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : Nat.floor ⁻¹' {0} = Set.Iio 1

theorem Nat.preimage_floor_of_ne_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {n : ℕ} (hn : n ≠ 0) : Nat.floor ⁻¹' {n} = Set.Ico (↑n) (↑n + 1)

Ceil

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

theorem Nat.add_one_le_ceil_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} : n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a

@[simp]

theorem Nat.one_le_ceil_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} : 1 ≤ ⌈a⌉₊ ↔ 0 < a

theorem Nat.ceil_le_floor_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) : ⌈a⌉₊ ≤ ⌊a⌋₊ + 1

theorem Nat.le_ceil {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) : a ≤ ↑⌈a⌉₊

@[simp]

theorem Nat.ceil_intCast {α : Type u_4} [LinearOrderedRing α] [FloorSemiring α] (z : ℤ) : ⌈↑z⌉₊ = z.toNat

@[simp]

theorem Nat.ceil_natCast {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) : ⌈↑n⌉₊ = n

theorem Nat.ceil_mono {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : Monotone Nat.ceil

theorem Nat.ceil_le_ceil {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (hab : a ≤ b) : ⌈a⌉₊ ≤ ⌈b⌉₊

@[simp]

theorem Nat.ceil_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : ⌈0⌉₊ = 0

@[simp]

theorem Nat.ceil_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : ⌈1⌉₊ = 1

@[simp]

theorem Nat.ceil_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (n : ℕ) [n.AtLeastTwo] : ⌈OfNat.ofNat n⌉₊ = n

@[simp]

theorem Nat.ceil_eq_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} : ⌈a⌉₊ = 0 ↔ a ≤ 0

@[simp]

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

theorem Nat.lt_of_ceil_lt {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (h : ⌈a⌉₊ < n) : a < ↑n

theorem Nat.le_of_ceil_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (h : ⌈a⌉₊ ≤ n) : a ≤ ↑n

theorem Nat.floor_le_ceil {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) : ⌊a⌋₊ ≤ ⌈a⌉₊

theorem Nat.floor_lt_ceil_of_lt_of_pos {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (h : a < b) (h' : 0 < b) : ⌊a⌋₊ < ⌈b⌉₊

theorem Nat.ceil_eq_iff {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {n : ℕ} (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n

@[simp]

theorem Nat.preimage_ceil_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] : Nat.ceil ⁻¹' {0} = Set.Iic 0

theorem Nat.preimage_ceil_of_ne_zero {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {n : ℕ} (hn : n ≠ 0) : Nat.ceil ⁻¹' {n} = Set.Ioc ↑(n - 1) ↑n

Intervals

@[simp]

theorem Nat.preimage_Ioo {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (ha : 0 ≤ a) : Nat.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋₊ ⌈b⌉₊

@[simp]

theorem Nat.preimage_Ico {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} : Nat.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉₊ ⌈b⌉₊

@[simp]

theorem Nat.preimage_Ioc {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : Nat.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋₊ ⌊b⌋₊

@[simp]

theorem Nat.preimage_Icc {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} {b : α} (hb : 0 ≤ b) : Nat.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉₊ ⌊b⌋₊

@[simp]

theorem Nat.preimage_Ioi {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : Nat.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋₊

@[simp]

theorem Nat.preimage_Ici {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} : Nat.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉₊

@[simp]

theorem Nat.preimage_Iio {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} : Nat.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉₊

@[simp]

theorem Nat.preimage_Iic {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : Nat.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋₊

theorem Nat.floor_add_nat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) (n : ℕ) : ⌊a + ↑n⌋₊ = ⌊a⌋₊ + n

theorem Nat.floor_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : ⌊a + 1⌋₊ = ⌊a⌋₊ + 1

theorem Nat.floor_add_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] : ⌊a + OfNat.ofNat n⌋₊ = ⌊a⌋₊ + OfNat.ofNat n

@[simp]

theorem Nat.floor_sub_nat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ℕ) : ⌊a - ↑n⌋₊ = ⌊a⌋₊ - n

@[simp]

theorem Nat.floor_sub_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) : ⌊a - 1⌋₊ = ⌊a⌋₊ - 1

@[simp]

theorem Nat.floor_sub_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] [Sub α] [OrderedSub α] [ExistsAddOfLE α] (a : α) (n : ℕ) [n.AtLeastTwo] : ⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n

theorem Nat.ceil_add_nat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) (n : ℕ) : ⌈a + ↑n⌉₊ = ⌈a⌉₊ + n

theorem Nat.ceil_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : ⌈a + 1⌉₊ = ⌈a⌉₊ + 1

theorem Nat.ceil_add_ofNat {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) (n : ℕ) [n.AtLeastTwo] : ⌈a + OfNat.ofNat n⌉₊ = ⌈a⌉₊ + OfNat.ofNat n

theorem Nat.ceil_lt_add_one {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] {a : α} (ha : 0 ≤ a) : ↑⌈a⌉₊ < a + 1

theorem Nat.ceil_add_le {α : Type u_2} [LinearOrderedSemiring α] [FloorSemiring α] (a : α) (b : α) : ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊

theorem Nat.sub_one_lt_floor {α : Type u_2} [LinearOrderedRing α] [FloorSemiring α] (a : α) : a - 1 < ↑⌊a⌋₊

theorem Nat.floor_div_nat {α : Type u_2} [LinearOrderedSemifield α] [FloorSemiring α] (a : α) (n : ℕ) : ⌊a / ↑n⌋₊ = ⌊a⌋₊ / n

theorem Nat.floor_div_ofNat {α : Type u_2} [LinearOrderedSemifield α] [FloorSemiring α] (a : α) (n : ℕ) [n.AtLeastTwo] : ⌊a / OfNat.ofNat n⌋₊ = ⌊a⌋₊ / OfNat.ofNat n

theorem Nat.floor_div_eq_div {α : Type u_2} [LinearOrderedSemifield α] [FloorSemiring α] (m : ℕ) (n : ℕ) : ⌊↑m / ↑n⌋₊ = m / n

Natural division is the floor of field division.

theorem Nat.mul_lt_floor {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} {b : α} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉₊ ≤ a) : b * a < ↑⌊a⌋₊

theorem Nat.ceil_lt_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} {b : α} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a) : ↑⌈a⌉₊ < b * a

theorem Nat.ceil_le_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} {b : α} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉₊ / b ≤ a) : ↑⌈a⌉₊ ≤ b * a

theorem Nat.div_two_lt_floor {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} (ha : 1 ≤ a) : a / 2 < ↑⌊a⌋₊

theorem Nat.ceil_lt_two_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} (ha : 2⁻¹ < a) : ↑⌈a⌉₊ < 2 * a

theorem Nat.ceil_le_two_mul {α : Type u_2} [LinearOrderedField α] [FloorSemiring α] {a : α} (ha : 2⁻¹ ≤ a) : ↑⌈a⌉₊ ≤ 2 * a

theorem subsingleton_floorSemiring {α : Type u_4} [LinearOrderedSemiring α] : Subsingleton (FloorSemiring α)

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

Floor rings

class FloorRing (α : Type u_4) [LinearOrderedRing α] : 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 FloorRing.floor

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

• gc_ceil_coe : GaloisConnection FloorRing.ceil Int.cast

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

theorem FloorRing.gc_coe_floor {α : Type u_4} : ∀ {inst : LinearOrderedRing α} [self : FloorRing α], GaloisConnection Int.cast FloorRing.floor

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

theorem FloorRing.gc_ceil_coe {α : Type u_4} : ∀ {inst : LinearOrderedRing α} [self : FloorRing α], GaloisConnection FloorRing.ceil Int.cast

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

instance instFloorRingInt : FloorRing ℤ

Equations

• instFloorRingInt = { floor := id, ceil := id, gc_coe_floor := instFloorRingInt.proof_1, gc_ceil_coe := instFloorRingInt.proof_2 }

def FloorRing.ofFloor (α : Type u_4) [LinearOrderedRing α] (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 := ⋯ }

def FloorRing.ofCeil (α : Type u_4) [LinearOrderedRing α] (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 }

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

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

Equations

• Int.floor = FloorRing.floor

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

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

Equations

• Int.ceil = FloorRing.ceil

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

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

Equations

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

@[simp]

theorem Int.floor_int : Int.floor = id

@[simp]

theorem Int.ceil_int : Int.ceil = id

@[simp]

theorem Int.fract_int : Int.fract = 0

@[simp]

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

@[simp]

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

Floor

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

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

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

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

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

@[simp]

theorem Int.floor_le_sub_one_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : ℤ} {a : α} : ⌊a⌋ ≤ z - 1 ↔ a < ↑z

@[simp]

theorem Int.floor_le_neg_one_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : ⌊a⌋ ≤ -1 ↔ a < 0

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

theorem Int.lt_succ_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : a < ↑⌊a⌋.succ

@[simp]

theorem Int.lt_floor_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : a < ↑⌊a⌋ + 1

@[simp]

theorem Int.sub_one_lt_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : a - 1 < ↑⌊a⌋

@[simp]

theorem Int.floor_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ℤ) : ⌊↑z⌋ = z

@[simp]

theorem Int.floor_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) : ⌊↑n⌋ = ↑n

@[simp]

theorem Int.floor_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : ⌊0⌋ = 0

@[simp]

theorem Int.floor_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : ⌊1⌋ = 1

@[simp]

theorem Int.floor_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] : ⌊OfNat.ofNat n⌋ = ↑n

theorem Int.floor_mono {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : Monotone Int.floor

theorem Int.floor_le_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} (hab : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋

theorem Int.floor_pos {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : 0 < ⌊a⌋ ↔ 1 ≤ a

@[simp]

theorem Int.floor_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ℤ) : ⌊a + ↑z⌋ = ⌊a⌋ + z

@[simp]

theorem Int.floor_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌊a + 1⌋ = ⌊a⌋ + 1

theorem Int.le_floor_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : ⌊a⌋ + ⌊b⌋ ≤ ⌊a + b⌋

theorem Int.le_floor_add_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : ⌊a + b⌋ - 1 ≤ ⌊a⌋ + ⌊b⌋

@[simp]

theorem Int.floor_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ℤ) (a : α) : ⌊↑z + a⌋ = z + ⌊a⌋

@[simp]

theorem Int.floor_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) : ⌊a + ↑n⌋ = ⌊a⌋ + ↑n

@[simp]

theorem Int.floor_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) [n.AtLeastTwo] : ⌊a + OfNat.ofNat n⌋ = ⌊a⌋ + OfNat.ofNat n

@[simp]

theorem Int.floor_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) (a : α) : ⌊↑n + a⌋ = ↑n + ⌊a⌋

@[simp]

theorem Int.floor_ofNat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] (a : α) : ⌊OfNat.ofNat n + a⌋ = OfNat.ofNat n + ⌊a⌋

@[simp]

theorem Int.floor_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ℤ) : ⌊a - ↑z⌋ = ⌊a⌋ - z

@[simp]

theorem Int.floor_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) : ⌊a - ↑n⌋ = ⌊a⌋ - ↑n

@[simp]

theorem Int.floor_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌊a - 1⌋ = ⌊a⌋ - 1

@[simp]

theorem Int.floor_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) [n.AtLeastTwo] : ⌊a - OfNat.ofNat n⌋ = ⌊a⌋ - OfNat.ofNat n

theorem Int.abs_sub_lt_one_of_floor_eq_floor {α : Type u_4} [LinearOrderedCommRing α] [FloorRing α] {a : α} {b : α} (h : ⌊a⌋ = ⌊b⌋) : |a - b| < 1

theorem Int.floor_eq_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : ℤ} {a : α} : ⌊a⌋ = z ↔ ↑z ≤ a ∧ a < ↑z + 1

@[simp]

theorem Int.floor_eq_zero_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : ⌊a⌋ = 0 ↔ a ∈ Set.Ico 0 1

theorem Int.floor_eq_on_Ico {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℤ) (a : α) : a ∈ Set.Ico (↑n) (↑n + 1) → ⌊a⌋ = n

theorem Int.floor_eq_on_Ico' {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℤ) (a : α) : a ∈ Set.Ico (↑n) (↑n + 1) → ↑⌊a⌋ = ↑n

@[simp]

theorem Int.preimage_floor_singleton {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (m : ℤ) : Int.floor ⁻¹' {m} = Set.Ico (↑m) (↑m + 1)

Fractional part

@[simp]

theorem Int.self_sub_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : a - ↑⌊a⌋ = Int.fract a

@[simp]

theorem Int.floor_add_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ↑⌊a⌋ + Int.fract a = a

@[simp]

theorem Int.fract_add_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract a + ↑⌊a⌋ = a

@[simp]

theorem Int.fract_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (m : ℤ) : Int.fract (a + ↑m) = Int.fract a

@[simp]

theorem Int.fract_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (m : ℕ) : Int.fract (a + ↑m) = Int.fract a

@[simp]

theorem Int.fract_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract (a + 1) = Int.fract a

@[simp]

theorem Int.fract_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) [n.AtLeastTwo] : Int.fract (a + OfNat.ofNat n) = Int.fract a

@[simp]

theorem Int.fract_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (m : ℤ) (a : α) : Int.fract (↑m + a) = Int.fract a

@[simp]

theorem Int.fract_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) (a : α) : Int.fract (↑n + a) = Int.fract a

@[simp]

theorem Int.fract_one_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract (1 + a) = Int.fract a

@[simp]

theorem Int.fract_ofNat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] (a : α) : Int.fract (OfNat.ofNat n + a) = Int.fract a

@[simp]

theorem Int.fract_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (m : ℤ) : Int.fract (a - ↑m) = Int.fract a

@[simp]

theorem Int.fract_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) : Int.fract (a - ↑n) = Int.fract a

@[simp]

theorem Int.fract_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract (a - 1) = Int.fract a

@[simp]

theorem Int.fract_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) [n.AtLeastTwo] : Int.fract (a - OfNat.ofNat n) = Int.fract a

theorem Int.fract_add_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : Int.fract (a + b) ≤ Int.fract a + Int.fract b

theorem Int.fract_add_fract_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : Int.fract a + Int.fract b ≤ Int.fract (a + b) + 1

@[simp]

theorem Int.self_sub_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : a - Int.fract a = ↑⌊a⌋

@[simp]

theorem Int.fract_sub_self {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract a - a = -↑⌊a⌋

@[simp]

theorem Int.fract_nonneg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : 0 ≤ Int.fract a

theorem Int.fract_pos {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : 0 < Int.fract a ↔ a ≠ ↑⌊a⌋

The fractional part of a is positive if and only if a ≠ ⌊a⌋.

theorem Int.fract_lt_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract a < 1

@[simp]

theorem Int.fract_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : Int.fract 0 = 0

@[simp]

theorem Int.fract_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : Int.fract 1 = 0

theorem Int.abs_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : |Int.fract a| = Int.fract a

@[simp]

theorem Int.abs_one_sub_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : |1 - Int.fract a| = 1 - Int.fract a

@[simp]

theorem Int.fract_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ℤ) : Int.fract ↑z = 0

@[simp]

theorem Int.fract_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) : Int.fract ↑n = 0

@[simp]

theorem Int.fract_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] : Int.fract (OfNat.ofNat n) = 0

theorem Int.fract_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract ↑⌊a⌋ = 0

@[simp]

theorem Int.floor_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌊Int.fract a⌋ = 0

theorem Int.fract_eq_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} : Int.fract a = b ↔ 0 ≤ b ∧ b < 1 ∧ ∃ (z : ℤ), a - b = ↑z

theorem Int.fract_eq_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} : Int.fract a = Int.fract b ↔ ∃ (z : ℤ), a - b = ↑z

@[simp]

theorem Int.fract_eq_self {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : Int.fract a = a ↔ 0 ≤ a ∧ a < 1

@[simp]

theorem Int.fract_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract (Int.fract a) = Int.fract a

theorem Int.fract_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : ∃ (z : ℤ), Int.fract (a + b) - Int.fract a - Int.fract b = ↑z

theorem Int.fract_neg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {x : α} (hx : Int.fract x ≠ 0) : Int.fract (-x) = 1 - Int.fract x

@[simp]

theorem Int.fract_neg_eq_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {x : α} : Int.fract (-x) = 0 ↔ Int.fract x = 0

theorem Int.fract_mul_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : ℕ) : ∃ (z : ℤ), Int.fract a * ↑b - Int.fract (a * ↑b) = ↑z

theorem Int.preimage_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (s : Set α) : Int.fract ⁻¹' s = ⋃ (m : ℤ), (fun (x : α) => x - ↑m) ⁻¹' (s ∩ Set.Ico 0 1)

theorem Int.image_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (s : Set α) : Int.fract '' s = ⋃ (m : ℤ), (fun (x : α) => x - ↑m) '' s ∩ Set.Ico 0 1

theorem Int.fract_div_mul_self_mem_Ico {k : Type u_4} [LinearOrderedField k] [FloorRing k] (a : k) (b : k) (ha : 0 < a) : Int.fract (b / a) * a ∈ Set.Ico 0 a

theorem Int.fract_div_mul_self_add_zsmul_eq {k : Type u_4} [LinearOrderedField k] [FloorRing k] (a : k) (b : k) (ha : a ≠ 0) : Int.fract (b / a) * a + ⌊b / a⌋ • a = b

theorem Int.sub_floor_div_mul_nonneg {k : Type u_4} [LinearOrderedField k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) : 0 ≤ a - ↑⌊a / b⌋ * b

theorem Int.sub_floor_div_mul_lt {k : Type u_4} [LinearOrderedField k] [FloorRing k] {b : k} (a : k) (hb : 0 < b) : a - ↑⌊a / b⌋ * b < b

theorem Int.fract_div_natCast_eq_div_natCast_mod {k : Type u_4} [LinearOrderedField k] [FloorRing k] {m : ℕ} {n : ℕ} : Int.fract (↑m / ↑n) = ↑(m % n) / ↑n

theorem Int.fract_div_intCast_eq_div_intCast_mod {k : Type u_4} [LinearOrderedField k] [FloorRing k] {m : ℤ} {n : ℕ} : Int.fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Ceil

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

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

theorem Int.floor_neg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : ⌊-a⌋ = -⌈a⌉

theorem Int.ceil_neg {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : ⌈-a⌉ = -⌊a⌋

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

@[simp]

theorem Int.add_one_le_ceil_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : ℤ} {a : α} : z + 1 ≤ ⌈a⌉ ↔ ↑z < a

@[simp]

theorem Int.one_le_ceil_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : 1 ≤ ⌈a⌉ ↔ 0 < a

theorem Int.ceil_le_floor_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌈a⌉ ≤ ⌊a⌋ + 1

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

theorem Int.le_ceil_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : ℤ} {a : α} : z ≤ ⌈a⌉ ↔ ↑z - 1 < a

theorem Int.ceil_lt_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : ℤ} {a : α} : ⌈a⌉ < z ↔ a ≤ ↑z - 1

@[simp]

theorem Int.ceil_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ℤ) : ⌈↑z⌉ = z

@[simp]

theorem Int.ceil_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) : ⌈↑n⌉ = ↑n

@[simp]

theorem Int.ceil_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] : ⌈OfNat.ofNat n⌉ = ↑n

theorem Int.ceil_mono {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : Monotone Int.ceil

theorem Int.ceil_le_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} (hab : a ≤ b) : ⌈a⌉ ≤ ⌈b⌉

@[simp]

theorem Int.ceil_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ℤ) : ⌈a + ↑z⌉ = ⌈a⌉ + z

@[simp]

theorem Int.ceil_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) : ⌈a + ↑n⌉ = ⌈a⌉ + ↑n

@[simp]

theorem Int.ceil_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌈a + 1⌉ = ⌈a⌉ + 1

@[simp]

theorem Int.ceil_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) [n.AtLeastTwo] : ⌈a + OfNat.ofNat n⌉ = ⌈a⌉ + OfNat.ofNat n

@[simp]

theorem Int.ceil_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (z : ℤ) : ⌈a - ↑z⌉ = ⌈a⌉ - z

@[simp]

theorem Int.ceil_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) : ⌈a - ↑n⌉ = ⌈a⌉ - ↑n

@[simp]

theorem Int.ceil_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌈a - 1⌉ = ⌈a⌉ - 1

@[simp]

theorem Int.ceil_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (n : ℕ) [n.AtLeastTwo] : ⌈a - OfNat.ofNat n⌉ = ⌈a⌉ - OfNat.ofNat n

theorem Int.ceil_lt_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ↑⌈a⌉ < a + 1

theorem Int.ceil_add_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉

theorem Int.ceil_add_ceil_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) (b : α) : ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

@[simp]

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

@[simp]

theorem Int.ceil_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : ⌈0⌉ = 0

@[simp]

theorem Int.ceil_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : ⌈1⌉ = 1

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

theorem Int.ceil_eq_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {z : ℤ} {a : α} : ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ ↑z

@[simp]

theorem Int.ceil_eq_zero_iff {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : ⌈a⌉ = 0 ↔ a ∈ Set.Ioc (-1) 0

theorem Int.ceil_eq_on_Ioc {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ℤ) (a : α) : a ∈ Set.Ioc (↑z - 1) ↑z → ⌈a⌉ = z

theorem Int.ceil_eq_on_Ioc' {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (z : ℤ) (a : α) : a ∈ Set.Ioc (↑z - 1) ↑z → ↑⌈a⌉ = ↑z

theorem Int.floor_le_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : ⌊a⌋ ≤ ⌈a⌉

theorem Int.floor_lt_ceil_of_lt {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} (h : a < b) : ⌊a⌋ < ⌈b⌉

@[simp]

theorem Int.preimage_ceil_singleton {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (m : ℤ) : Int.ceil ⁻¹' {m} = Set.Ioc (↑m - 1) ↑m

theorem Int.fract_eq_zero_or_add_one_sub_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : Int.fract a = 0 ∨ Int.fract a = a + 1 - ↑⌈a⌉

theorem Int.ceil_eq_add_one_sub_fract {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : Int.fract a ≠ 0) : ↑⌈a⌉ = a + 1 - Int.fract a

theorem Int.ceil_sub_self_eq {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : Int.fract a ≠ 0) : ↑⌈a⌉ - a = 1 - Int.fract a

theorem Int.mul_lt_floor {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} {b : k} (hb₀ : 0 < b) (hb : b < 1) (hba : ↑⌈b / (1 - b)⌉ ≤ a) : b * a < ↑⌊a⌋

theorem Int.ceil_div_ceil_inv_sub_one {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 1 ≤ a) : ⌈↑⌈(a - 1)⁻¹⌉ / a⌉ = ⌈(a - 1)⁻¹⌉

theorem Int.ceil_lt_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} {b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b < a) : ↑⌈a⌉ < b * a

theorem Int.ceil_le_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} {b : k} (hb : 1 < b) (hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ a) : ↑⌈a⌉ ≤ b * a

theorem Int.div_two_lt_floor {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 1 ≤ a) : a / 2 < ↑⌊a⌋

theorem Int.ceil_lt_two_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 2⁻¹ < a) : ↑⌈a⌉ < 2 * a

theorem Int.ceil_le_two_mul {k : Type u_4} [LinearOrderedField k] [FloorRing k] {a : k} (ha : 2⁻¹ ≤ a) : ↑⌈a⌉ ≤ 2 * a

Intervals

@[simp]

theorem Int.preimage_Ioo {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} : Int.cast ⁻¹' Set.Ioo a b = Set.Ioo ⌊a⌋ ⌈b⌉

@[simp]

theorem Int.preimage_Ico {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} : Int.cast ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ ⌈b⌉

@[simp]

theorem Int.preimage_Ioc {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} : Int.cast ⁻¹' Set.Ioc a b = Set.Ioc ⌊a⌋ ⌊b⌋

@[simp]

theorem Int.preimage_Icc {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} {b : α} : Int.cast ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋

@[simp]

theorem Int.preimage_Ioi {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : Int.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋

@[simp]

theorem Int.preimage_Ici {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : Int.cast ⁻¹' Set.Ici a = Set.Ici ⌈a⌉

@[simp]

theorem Int.preimage_Iio {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : Int.cast ⁻¹' Set.Iio a = Set.Iio ⌈a⌉

@[simp]

theorem Int.preimage_Iic {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} : Int.cast ⁻¹' Set.Iic a = Set.Iic ⌊a⌋

Round

def round {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) : ℤ

round rounds a number to the nearest integer. round (1 / 2) = 1

Equations

• round x = if 2 * Int.fract x < 1 then ⌊x⌋ else ⌈x⌉

@[simp]

theorem round_zero {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : round 0 = 0

@[simp]

theorem round_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : round 1 = 1

@[simp]

theorem round_natCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) : round ↑n = ↑n

@[simp]

theorem round_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] : round (OfNat.ofNat n) = ↑n

@[simp]

theorem round_intCast {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℤ) : round ↑n = n

@[simp]

theorem round_add_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) : round (x + ↑y) = round x + y

@[simp]

theorem round_add_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : round (a + 1) = round a + 1

@[simp]

theorem round_sub_int {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) : round (x - ↑y) = round x - y

@[simp]

theorem round_sub_one {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (a : α) : round (a - 1) = round a - 1

@[simp]

theorem round_add_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) : round (x + ↑y) = round x + ↑y

@[simp]

theorem round_add_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (n : ℕ) [n.AtLeastTwo] : round (x + OfNat.ofNat n) = round x + OfNat.ofNat n

@[simp]

theorem round_sub_nat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) : round (x - ↑y) = round x - ↑y

@[simp]

theorem round_sub_ofNat {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (n : ℕ) [n.AtLeastTwo] : round (x - OfNat.ofNat n) = round x - OfNat.ofNat n

@[simp]

theorem round_int_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℤ) : round (↑y + x) = y + round x

@[simp]

theorem round_nat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (y : ℕ) : round (↑y + x) = ↑y + round x

@[simp]

theorem round_ofNat_add {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (n : ℕ) [n.AtLeastTwo] (x : α) : round (OfNat.ofNat n + x) = OfNat.ofNat n + round x

theorem abs_sub_round_eq_min {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) : |x - ↑(round x)| = min (Int.fract x) (1 - Int.fract x)

theorem round_le {α : Type u_2} [LinearOrderedRing α] [FloorRing α] (x : α) (z : ℤ) : |x - ↑(round x)| ≤ |x - ↑z|

theorem round_eq {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) : round x = ⌊x + 1 / 2⌋

@[simp]

theorem round_two_inv {α : Type u_2} [LinearOrderedField α] [FloorRing α] : round 2⁻¹ = 1

@[simp]

theorem round_neg_two_inv {α : Type u_2} [LinearOrderedField α] [FloorRing α] : round (-2⁻¹) = 0

@[simp]

theorem round_eq_zero_iff {α : Type u_2} [LinearOrderedField α] [FloorRing α] {x : α} : round x = 0 ↔ x ∈ Set.Ico (-(1 / 2)) (1 / 2)

theorem abs_sub_round {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) : |x - ↑(round x)| ≤ 1 / 2

theorem abs_sub_round_div_natCast_eq {α : Type u_2} [LinearOrderedField α] [FloorRing α] {m : ℕ} {n : ℕ} : |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

theorem sub_half_lt_round {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) : x - 1 / 2 < ↑(round x)

theorem round_le_add_half {α : Type u_2} [LinearOrderedField α] [FloorRing α] (x : α) : ↑(round x) ≤ x + 1 / 2

theorem Nat.floor_congr {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] {a : α} {b : β} (h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b) : ⌊a⌋₊ = ⌊b⌋₊

theorem Nat.ceil_congr {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] {a : α} {b : β} (h : ∀ (n : ℕ), a ≤ ↑n ↔ b ≤ ↑n) : ⌈a⌉₊ = ⌈b⌉₊

theorem Nat.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : ⌊f a⌋₊ = ⌊a⌋₊

theorem Nat.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedSemiring α] [LinearOrderedSemiring β] [FloorSemiring α] [FloorSemiring β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : ⌈f a⌉₊ = ⌈a⌉₊

theorem Int.floor_congr {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] {a : α} {b : β} (h : ∀ (n : ℤ), ↑n ≤ a ↔ ↑n ≤ b) : ⌊a⌋ = ⌊b⌋

theorem Int.ceil_congr {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] {a : α} {b : β} (h : ∀ (n : ℤ), a ≤ ↑n ↔ b ≤ ↑n) : ⌈a⌉ = ⌈b⌉

theorem Int.map_floor {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : ⌊f a⌋ = ⌊a⌋

theorem Int.map_ceil {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : ⌈f a⌉ = ⌈a⌉

theorem Int.map_fract {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedRing α] [LinearOrderedRing β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : Int.fract (f a) = f (Int.fract a)

theorem Int.map_round {F : Type u_1} {α : Type u_2} {β : Type u_3} [LinearOrderedField α] [LinearOrderedField β] [FloorRing α] [FloorRing β] [FunLike F α β] [RingHomClass F α β] (f : F) (hf : StrictMono ⇑f) (a : α) : round (f a) = round a

A floor ring as a floor semiring

@[instance 100]

instance FloorRing.toFloorSemiring {α : Type u_2} [LinearOrderedRing α] [FloorRing α] : FloorSemiring α

Equations

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

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

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

@[simp]

theorem Nat.floor_int : Nat.floor = Int.toNat

@[simp]

theorem Nat.ceil_int : Nat.ceil = Int.toNat

theorem Int.natCast_floor_eq_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) : ↑⌊a⌋₊ = ⌊a⌋

theorem Int.natCast_ceil_eq_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) : ↑⌈a⌉₊ = ⌈a⌉

theorem natCast_floor_eq_intCast_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) : ↑⌊a⌋₊ = ↑⌊a⌋

theorem natCast_ceil_eq_intCast_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) : ↑⌈a⌉₊ = ↑⌈a⌉

@[deprecated Int.natCast_floor_eq_floor]

theorem Int.ofNat_floor_eq_floor {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) : ↑⌊a⌋₊ = ⌊a⌋

Alias of Int.natCast_floor_eq_floor.

@[deprecated Int.natCast_ceil_eq_ceil]

theorem Int.ofNat_ceil_eq_ceil {α : Type u_2} [LinearOrderedRing α] [FloorRing α] {a : α} (ha : 0 ≤ a) : ↑⌈a⌉₊ = ⌈a⌉

Alias of Int.natCast_ceil_eq_ceil.

theorem subsingleton_floorRing {α : Type u_4} [LinearOrderedRing α] : Subsingleton (FloorRing α)

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

def Mathlib.Meta.Positivity.evalIntFloor : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: Int.floor is nonnegative if its input is.

def Mathlib.Meta.Positivity.evalNatCeil : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: Nat.ceil is positive if its input is.

def Mathlib.Meta.Positivity.evalIntCeil : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: Int.ceil is positive/nonnegative if its input is.