Decomposing a locally finite ordered ring into boxes

This file proves that any locally finite ordered ring can be decomposed into "boxes", namely differences of consecutive intervals.

Implementation notes

We don't need the full ring structure, only that there is an order embedding ℤ →

General locally finite ordered ring

def Finset.box {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] : ℕ → Finset α

Hollow box centered at 0 : α going from -n to n.

Equations

• Finset.box = disjointed fun (n : ℕ) => Finset.Icc (-↑n) ↑n

@[simp]

theorem Finset.box_zero {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] : Finset.box 0 = {0}

theorem Finset.box_succ_eq_sdiff {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) : Finset.box (n + 1) = Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n) \ Finset.Icc (-↑n) ↑n

theorem Finset.disjoint_box_succ_prod {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) : Disjoint (Finset.box (n + 1)) (Finset.Icc (-↑n) ↑n)

@[simp]

theorem Finset.box_succ_union_prod {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) : Finset.box (n + 1) ∪ Finset.Icc (-↑n) ↑n = Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n)

theorem Finset.box_succ_disjUnion {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] (n : ℕ) : Finset.disjUnion (Finset.box (n + 1)) (Finset.Icc (-↑n) ↑n) ⋯ = Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n)

@[simp]

theorem Finset.zero_mem_box {α : Type u_1} [OrderedRing α] [LocallyFiniteOrder α] [DecidableEq α] {n : ℕ} : 0 ∈ Finset.box n ↔ n = 0

Product of locally finite ordered rings

@[simp]

theorem Prod.card_box_succ {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedRing β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableEq α] [DecidableEq β] [DecidableRel fun (x x_1 : α × β) => x ≤ x_1] (n : ℕ) : (Finset.box (n + 1)).card = (Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n)).card * (Finset.Icc (-↑(Nat.succ n)) ↑(Nat.succ n)).card - (Finset.Icc (-↑n) ↑n).card * (Finset.Icc (-↑n) ↑n).card

ℤ × ℤ

theorem Int.card_box {n : ℕ} : n ≠ 0 → (Finset.box n).card = 8 * n

@[simp]

theorem Int.mem_box {x : ℤ × ℤ} {n : ℕ} : x ∈ Finset.box n ↔ max (Int.natAbs x.1) (Int.natAbs x.2) = n

theorem Int.existsUnique_mem_box (x : ℤ × ℤ) : ∃! (n : ℕ), x ∈ Finset.box n