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) [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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.

class CeilDiv (α : Type u_2) (β : Type u_3) [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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.

def «term_⌊/⌋_» : Lean.TrailingParserDescr

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

def «term_⌈/⌉_» : Lean.TrailingParserDescr

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

theorem gc_floorDiv_smul {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] {a : α} (ha : a ≤ 0) (b : β) : b ⌊/⌋ a = 0

theorem floorDiv_zero {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] (b : β) : b ⌊/⌋ 0 = 0

@[simp]

theorem zero_floorDiv {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] (a : α) : 0 ⌊/⌋ a = 0

theorem smul_floorDiv_le {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] {a : α} {b : β} (ha : 0 < a) : a • (b ⌊/⌋ a) ≤ b

theorem gc_smul_ceilDiv {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] {a : α} (ha : a ≤ 0) (b : β) : b ⌈/⌉ a = 0

theorem ceilDiv_zero {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] (b : β) : b ⌈/⌉ 0 = 0

@[simp]

theorem zero_ceilDiv {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] (a : α) : 0 ⌈/⌉ a = 0

theorem le_smul_ceilDiv {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] {a : α} {b : β} (ha : 0 < a) : b ≤ a • (b ⌈/⌉ a)

theorem floorDiv_le_ceilDiv {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [LinearOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [PosSMulReflectLE α β] [FloorDiv α β] [CeilDiv α β] {a : α} {b : β} : b ⌊/⌋ a ≤ b ⌈/⌉ a

@[simp]

theorem floorDiv_one {α : Type u_2} {β : Type u_3} [Semiring α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [MulActionWithZero α β] [FloorDiv α β] [IsOrderedRing α] [Nontrivial α] (b : β) : b ⌊/⌋ 1 = b

@[simp]

theorem smul_floorDiv {α : Type u_2} {β : Type u_3} [Semiring α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [MulActionWithZero α β] [FloorDiv α β] {a : α} [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) : a • b ⌊/⌋ a = b

@[simp]

theorem ceilDiv_one {α : Type u_2} {β : Type u_3} [Semiring α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [MulActionWithZero α β] [CeilDiv α β] [IsOrderedRing α] [Nontrivial α] (b : β) : b ⌈/⌉ 1 = b

@[simp]

theorem smul_ceilDiv {α : Type u_2} {β : Type u_3} [Semiring α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [MulActionWithZero α β] [CeilDiv α β] {a : α} [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) : a • b ⌈/⌉ a = b

theorem gc_floorDiv_mul {α : Type u_2} [Semiring α] [PartialOrder α] [FloorDiv α α] {a : α} (ha : 0 < a) : GaloisConnection (fun (x : α) => a * x) fun (x : α) => x ⌊/⌋ a

theorem le_floorDiv_iff_mul_le {α : Type u_2} [Semiring α] [PartialOrder α] [FloorDiv α α] {a b c : α} (ha : 0 < a) : c ≤ b ⌊/⌋ a ↔ a • c ≤ b

theorem gc_mul_ceilDiv {α : Type u_2} [Semiring α] [PartialOrder α] [CeilDiv α α] {a : α} (ha : 0 < a) : GaloisConnection (fun (x : α) => x ⌈/⌉ a) fun (x : α) => a * x

theorem ceilDiv_le_iff_le_mul {α : Type u_2} [Semiring α] [PartialOrder α] [CeilDiv α α] {a b c : α} (ha : 0 < a) : b ⌈/⌉ a ≤ c ↔ b ≤ a * c

instance Nat.instFloorDiv : FloorDiv ℕ ℕ

instance Nat.instCeilDiv : CeilDiv ℕ ℕ

@[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} [AddCommMonoid α] [PartialOrder α] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → PartialOrder (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → FloorDiv α (π i)] : FloorDiv α ((i : ι) → π i)

theorem Pi.floorDiv_def {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [AddCommMonoid α] [PartialOrder α] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → PartialOrder (π 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} [AddCommMonoid α] [PartialOrder α] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → PartialOrder (π 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} [AddCommMonoid α] [PartialOrder α] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → PartialOrder (π i)] [(i : ι) → SMulZeroClass α (π i)] [(i : ι) → CeilDiv α (π i)] : CeilDiv α ((i : ι) → π i)

theorem Pi.ceilDiv_def {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [AddCommMonoid α] [PartialOrder α] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → PartialOrder (π 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} [AddCommMonoid α] [PartialOrder α] [(i : ι) → AddCommMonoid (π i)] [(i : ι) → PartialOrder (π 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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] : FloorDiv α (ι →₀ β)

theorem Finsupp.floorDiv_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] (f : ι →₀ β) (a : α) : f ⌊/⌋ a = mapRange (fun (x : β) => x ⌊/⌋ a) ⋯ f

theorem Finsupp.coe_floorDiv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [FloorDiv α β] {f : ι →₀ β} {a : α} : (f ⌊/⌋ a).support ⊆ f.support

noncomputable instance Finsupp.instCeilDiv {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] : CeilDiv α (ι →₀ β)

theorem Finsupp.ceilDiv_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] (f : ι →₀ β) (a : α) : f ⌈/⌉ a = mapRange (fun (x : β) => x ⌈/⌉ a) ⋯ f

theorem Finsupp.coe_ceilDiv_def {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [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} [AddCommMonoid α] [PartialOrder α] [AddCommMonoid β] [PartialOrder β] [SMulZeroClass α β] [CeilDiv α β] {f : ι →₀ β} {a : α} : (f ⌈/⌉ a).support ⊆ f.support