A common offset for integer rounding

Signed Euclidean division by a positive integer is floor division. Averaging over all offsets recovers the original integer, and the total rounded absolute difference recovers the original absolute difference. Consequently a family of endpoint differences with total absolute value less than the denominator has an offset that rounds every pair to equal integers.

The endpoint-slope bounds used in finite graph specialization are preserved by this same rounding, including negative heights and negative slopes.

def Utilities.CommonOffsetRounding.round (N : ℕ) (k : Fin N) (a : ℤ) : ℤ

Floor an integer after adding the chosen residue offset.

Equations

• Utilities.CommonOffsetRounding.round N k a = (a + ↑↑k) / ↑N

theorem Utilities.CommonOffsetRounding.round_mono (N : ℕ) (hN : 0 < N) (k : Fin N) {a b : ℤ} (hab : a ≤ b) : round N k a ≤ round N k b

theorem Utilities.CommonOffsetRounding.round_add_mul (N : ℕ) (hN : 0 < N) (k : Fin N) (a c : ℤ) : round N k (a + ↑N * c) = round N k a + c

An integral translation before rounding remains exact.

theorem Utilities.CommonOffsetRounding.sum_round (N : ℕ) (hN : 0 < N) (a : ℤ) : ∑ k : Fin N, round N k a = a

The sum over all residue offsets is the original signed integer.

theorem Utilities.CommonOffsetRounding.sum_abs_round_sub (N : ℕ) (hN : 0 < N) (a b : ℤ) : ∑ k : Fin N, |round N k a - round N k b| = |a - b|

The total absolute rounding discrepancy over all offsets equals the original absolute discrepancy. No bound on that discrepancy is required.

theorem Utilities.CommonOffsetRounding.exists_common_offset {ι : Type u_1} (N : ℕ) (hN : 0 < N) (F : Finset ι) (A B : ι → ℤ) (hBudget : ∑ e ∈ F, |A e - B e| < ↑N) : ∃ (k : Fin N), ∀ e ∈ F, round N k (A e) = round N k (B e)

If the total discrepancy of finitely many endpoint pairs is less than N, one common residue offset rounds all those pairs to equal integers.

theorem Utilities.CommonOffsetRounding.round_sub_bounds (N : ℕ) (hN : 0 < N) (k : Fin N) (A B a b : ℤ) (hlower : ↑N * a ≤ B - A) (hupper : B - A ≤ ↑N * b) : a ≤ round N k B - round N k A ∧ round N k B - round N k A ≤ b

Common-offset rounding preserves any integral lower and upper slope bounds on an endpoint difference across a path of length N.