Documentation

Mathlib.Algebra.Order.Floor.Div

Flooring, ceiling division #

This file defines division rounded up and down.

The setup is an ordered monoid α acting on an ordered monoid β. If a : α, b : β, we would like to be able to "divide" b by a, namely find c : β such that a • c = b. This is of course not always possible, but in some cases at least there is a least c such that b ≤ a • c and a greatest c such that a • c ≤ b. We call the first one the "ceiling division of b by a" and the second one the "flooring division of b by a"

If α and β are both ℕ, then one can check that our flooring and ceiling divisions really are the floor and ceil of the exact division. If α is ℕ and β is the functions ι → ℕ, then the flooring and ceiling divisions are taken pointwise.

In order theory terms, those operations are respectively the right and left adjoints to the map b ↦ a • b.

Main declarations #

FloorDiv: Typeclass for the existence of a flooring division, denoted b ⌊/⌋ a.
CeilDiv: Typeclass for the existence of a ceiling division, denoted b ⌈/⌉ a.

Note in both cases we only allow dividing by positive inputs. We enforce the following junk values:

b ⌊/⌋ a = b ⌈/⌉ a = 0 if a ≤ 0
0 ⌊/⌋ a = 0 ⌈/⌉ a = 0

Notation #

b ⌊/⌋ a for the flooring division of b by a
b ⌈/⌉ a for the ceiling division of b by a

TODO #

norm_num extension
Prove ⌈a / b⌉ = a ⌈/⌉ b when a, b : ℕ

class FloorDiv (α : Type u_2) (β : Type u_3) [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] :

Type (max u_2 u_3)

Typeclass for division rounded down. For each a > 0, this asserts the existence of a right adjoint to the map b ↦ a • b : β → β.

floorDiv : β → α → β
Flooring division. If a > 0, then b ⌊/⌋ a is the greatest c such that a • c ≤ b.
floorDiv_gc : ∀ ⦃a : α⦄, 0 < a → GaloisConnection (fun (x : β) => a • x) fun (x : β) => x ⌊/⌋ a
Do not use this. Use gc_floorDiv_smul or gc_floorDiv_mul instead.
floorDiv_nonpos : ∀ ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌊/⌋ a = 0
Do not use this. Use floorDiv_nonpos instead.
zero_floorDiv : ∀ (a : α), 0 ⌊/⌋ a = 0
Do not use this. Use zero_floorDiv instead.

Instances

class CeilDiv (α : Type u_2) (β : Type u_3) [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] :

Type (max u_2 u_3)

Typeclass for division rounded up. For each a > 0, this asserts the existence of a left adjoint to the map b ↦ a • b : β → β.

ceilDiv : β → α → β
Ceiling division. If a > 0, then b ⌈/⌉ a is the least c such that b ≤ a • c.
ceilDiv_gc : ∀ ⦃a : α⦄, 0 < a → GaloisConnection (fun (x : β) => x ⌈/⌉ a) fun (x : β) => a • x
Do not use this. Use gc_smul_ceilDiv or gc_mul_ceilDiv instead.
ceilDiv_nonpos : ∀ ⦃a : α⦄, a ≤ 0 → ∀ (b : β), b ⌈/⌉ a = 0
Do not use this. Use ceilDiv_nonpos instead.
zero_ceilDiv : ∀ (a : α), 0 ⌈/⌉ a = 0
Do not use this. Use zero_ceilDiv instead.

Instances

def «term_⌊/⌋_» :

Lean.TrailingParserDescr

Flooring division. If a > 0, then b ⌊/⌋ a is the greatest c such that a • c ≤ b.

Equations

«term_⌊/⌋_» = Lean.ParserDescr.trailingNode `term_⌊/⌋_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⌊/⌋ ") (Lean.ParserDescr.cat `term 71))

Instances For

def «term_⌈/⌉_» :

Lean.TrailingParserDescr

Ceiling division. If a > 0, then b ⌈/⌉ a is the least c such that b ≤ a • c.

Equations

«term_⌈/⌉_» = Lean.ParserDescr.trailingNode `term_⌈/⌉_ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⌈/⌉ ") (Lean.ParserDescr.cat `term 71))

Instances For

theorem gc_floorDiv_smul {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] {a : α} (ha : 0 < a) :

GaloisConnection (fun (x : β) => a • x) fun (x : β) => x ⌊/⌋ a

@[simp]

theorem le_floorDiv_iff_smul_le {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] {a : α} {b : β} {c : β} (ha : 0 < a) :

c ≤ b ⌊/⌋ a ↔ a • c ≤ b

@[simp]

theorem floorDiv_of_nonpos {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] {a : α} (ha : a ≤ 0) (b : β) :

b ⌊/⌋ a = 0

theorem floorDiv_zero {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] (b : β) :

b ⌊/⌋ 0 = 0

@[simp]

theorem zero_floorDiv {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] (a : α) :

0 ⌊/⌋ a = 0

theorem smul_floorDiv_le {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] {a : α} {b : β} (ha : 0 < a) :

a • (b ⌊/⌋ a) ≤ b

theorem gc_smul_ceilDiv {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] {a : α} (ha : 0 < a) :

GaloisConnection (fun (x : β) => x ⌈/⌉ a) fun (x : β) => a • x

@[simp]

theorem ceilDiv_le_iff_le_smul {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] {a : α} {b : β} {c : β} (ha : 0 < a) :

b ⌈/⌉ a ≤ c ↔ b ≤ a • c

@[simp]

theorem ceilDiv_of_nonpos {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] {a : α} (ha : a ≤ 0) (b : β) :

b ⌈/⌉ a = 0

theorem ceilDiv_zero {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] (b : β) :

b ⌈/⌉ 0 = 0

@[simp]

theorem zero_ceilDiv {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] (a : α) :

0 ⌈/⌉ a = 0

theorem le_smul_ceilDiv {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] {a : α} {b : β} (ha : 0 < a) :

b ≤ a • (b ⌈/⌉ a)

theorem floorDiv_le_ceilDiv {α : Type u_2} {β : Type u_3} [LinearOrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [PosSMulReflectLE α β] [FloorDiv α β] [CeilDiv α β] {a : α} {b : β} :

b ⌊/⌋ a ≤ b ⌈/⌉ a

@[simp]

theorem floorDiv_one {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedAddCommMonoid β] [MulActionWithZero α β] [FloorDiv α β] [Nontrivial α] (b : β) :

b ⌊/⌋ 1 = b

@[simp]

theorem smul_floorDiv {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedAddCommMonoid β] [MulActionWithZero α β] [FloorDiv α β] {a : α} [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) :

a • b ⌊/⌋ a = b

@[simp]

theorem ceilDiv_one {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedAddCommMonoid β] [MulActionWithZero α β] [CeilDiv α β] [Nontrivial α] (b : β) :

b ⌈/⌉ 1 = b

@[simp]

theorem smul_ceilDiv {α : Type u_2} {β : Type u_3} [OrderedSemiring α] [OrderedAddCommMonoid β] [MulActionWithZero α β] [CeilDiv α β] {a : α} [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) :

a • b ⌈/⌉ a = b

theorem gc_floorDiv_mul {α : Type u_2} [OrderedSemiring α] [FloorDiv α α] {a : α} (ha : 0 < a) :

GaloisConnection (fun (x : α) => a * x) fun (x : α) => x ⌊/⌋ a

theorem le_floorDiv_iff_mul_le {α : Type u_2} [OrderedSemiring α] [FloorDiv α α] {a : α} {b : α} {c : α} (ha : 0 < a) :

c ≤ b ⌊/⌋ a ↔ a • c ≤ b

theorem gc_mul_ceilDiv {α : Type u_2} [OrderedSemiring α] [CeilDiv α α] {a : α} (ha : 0 < a) :

GaloisConnection (fun (x : α) => x ⌈/⌉ a) fun (x : α) => a * x

theorem ceilDiv_le_iff_le_mul {α : Type u_2} [OrderedSemiring α] [CeilDiv α α] {a : α} {b : α} {c : α} (ha : 0 < a) :

b ⌈/⌉ a ≤ c ↔ b ≤ a * c

instance Nat.instFloorDiv :

FloorDiv ℕ ℕ

Equations

Nat.instFloorDiv = { floorDiv := HDiv.hDiv, floorDiv_gc := Nat.instFloorDiv.proof_1, floorDiv_nonpos := Nat.instFloorDiv.proof_2, zero_floorDiv := Nat.zero_div }

instance Nat.instCeilDiv :

CeilDiv ℕ ℕ

Equations

Nat.instCeilDiv = { ceilDiv := fun (a b : ℕ) => (a + b - 1) / b, ceilDiv_gc := Nat.instCeilDiv.proof_1, ceilDiv_nonpos := Nat.instCeilDiv.proof_2, zero_ceilDiv := Nat.instCeilDiv.proof_3 }

@[simp]

theorem Nat.floorDiv_eq_div (a : ℕ) (b : ℕ) :

a ⌊/⌋ b = a / b

theorem Nat.ceilDiv_eq_add_pred_div (a : ℕ) (b : ℕ) :

a ⌈/⌉ b = (a + b - 1) / b

instance Pi.instFloorDiv {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [OrderedAddCommMonoid α] [(i : ι) → OrderedAddCommMonoid (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → FloorDiv α (π i)] :

FloorDiv α ((i : ι) → π i)

Equations

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

theorem Pi.floorDiv_def {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [OrderedAddCommMonoid α] [(i : ι) → OrderedAddCommMonoid (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → FloorDiv α (π i)] (f : (i : ι) → π i) (a : α) :

f ⌊/⌋ a = fun (i : ι) => f i ⌊/⌋ a

@[simp]

theorem Pi.floorDiv_apply {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [OrderedAddCommMonoid α] [(i : ι) → OrderedAddCommMonoid (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → FloorDiv α (π i)] (f : (i : ι) → π i) (a : α) (i : ι) :

(f ⌊/⌋ a) i = f i ⌊/⌋ a

instance Pi.instCeilDiv {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [OrderedAddCommMonoid α] [(i : ι) → OrderedAddCommMonoid (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → CeilDiv α (π i)] :

CeilDiv α ((i : ι) → π i)

Equations

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

theorem Pi.ceilDiv_def {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [OrderedAddCommMonoid α] [(i : ι) → OrderedAddCommMonoid (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → CeilDiv α (π i)] (f : (i : ι) → π i) (a : α) :

f ⌈/⌉ a = fun (i : ι) => f i ⌈/⌉ a

@[simp]

theorem Pi.ceilDiv_apply {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [OrderedAddCommMonoid α] [(i : ι) → OrderedAddCommMonoid (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → CeilDiv α (π i)] (f : (i : ι) → π i) (a : α) (i : ι) :

(f ⌈/⌉ a) i = f i ⌈/⌉ a

noncomputable instance Finsupp.instFloorDiv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] :

FloorDiv α (ι →₀ β)

Equations

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

theorem Finsupp.floorDiv_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] (f : ι →₀ β) (a : α) :

f ⌊/⌋ a = Finsupp.mapRange (fun (x : β) => x ⌊/⌋ a) (_ : 0 ⌊/⌋ a = 0) f

theorem Finsupp.coe_floorDiv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] (f : ι →₀ β) (a : α) :

⇑(f ⌊/⌋ a) = fun (i : ι) => f i ⌊/⌋ a

@[simp]

theorem Finsupp.floorDiv_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] (f : ι →₀ β) (a : α) (i : ι) :

(f ⌊/⌋ a) i = f i ⌊/⌋ a

theorem Finsupp.support_floorDiv_subset {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [FloorDiv α β] {f : ι →₀ β} {a : α} :

(f ⌊/⌋ a).support ⊆ f.support

noncomputable instance Finsupp.instCeilDiv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] :

CeilDiv α (ι →₀ β)

Equations

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

theorem Finsupp.ceilDiv_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] (f : ι →₀ β) (a : α) :

f ⌈/⌉ a = Finsupp.mapRange (fun (x : β) => x ⌈/⌉ a) (_ : 0 ⌈/⌉ a = 0) f

theorem Finsupp.coe_ceilDiv_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] (f : ι →₀ β) (a : α) :

⇑(f ⌈/⌉ a) = fun (i : ι) => f i ⌈/⌉ a

@[simp]

theorem Finsupp.ceilDiv_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] (f : ι →₀ β) (a : α) (i : ι) :

(f ⌈/⌉ a) i = f i ⌈/⌉ a

theorem Finsupp.support_ceilDiv_subset {ι : Type u_1} {α : Type u_2} {β : Type u_3} [OrderedAddCommMonoid α] [OrderedAddCommMonoid β] [SMulZeroClass α β] [CeilDiv α β] {f : ι →₀ β} {a : α} :

(f ⌈/⌉ a).support ⊆ f.support