Round-to-multiple bounds and bucket refinement

Mirror of Mathlib/Algebra/Order/ToIntervalMod.lean: the additions a PR there would make. [UPSTREAM]

A width-ε bucket partition of a scale is the kernel of ⌊·/ε⌋ — the object linguistics calls scale granularity ([SS11], [Kri07a]). It is not the coset partition of ε·ℤ (AddSubgroup.zmultiples): cosets collect residues, buckets collect neighbours. Mathlib already provides the index and its bounds — toIcoDiv_eq_floor identifies toIcoDiv hε 0 with ⌊·/ε⌋, and sub_floor_div_mul_nonneg/sub_floor_div_mul_lt bound the cell — so this file adds only what is missing: the error bound for rounding to the nearest multiple of ε, and the refinement half of the finer-than order on bucket partitions, derived from the kernel keystone Setoid.ker_le_ker_comp via the floor-nesting identities (Nat.div_div_eq_div_mul, Int.floor_div_natCast).

Main results

• abs_sub_round_div_zsmul_le: rounding to the nearest multiple of ε moves a point by at most ε / 2
• Setoid.ker_floor_div_le_natCast_mul, Nat.ker_div_le_of_dvd: finer widths refine the bucket partition

theorem Nat.ker_div_le_of_dvd {ε₁ ε₂ : ℕ} (h : ε₁ ∣ ε₂) : (Setoid.ker fun (x : ℕ) => x / ε₁) ≤ Setoid.ker fun (x : ℕ) => x / ε₂

Finer grain widths refine the bucket partition on ℕ: if ε₁ ∣ ε₂, the ε₁-buckets sit inside the ε₂-buckets.

theorem Setoid.ker_floor_div_le_natCast_mul {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] (ε : α) (k : ℕ) : (ker fun (d : α) => ⌊d / ε⌋) ≤ ker fun (d : α) => ⌊d / (↑k * ε)⌋

Multiplying the width by a natural coarsens the bucket partition Setoid.ker ⌊·/ε⌋: the refinement half of the finer-than order, via the kernel keystone and Int.floor_div_natCast.

theorem abs_sub_round_div_zsmul_le {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {ε : α} (hε : 0 < ε) (d : α) : |d - round (d / ε) • ε| ≤ ε / 2

Rounding to the nearest multiple of ε moves a point by at most ε / 2 — the sibling of abs_sub_round for multiples.