Ceiling division lemmas

This file provides arithmetic lemmas relating ceiling division on natural numbers to inequalities in the extended natural numbers.

Main results

• ENat.natCast_le_nsmul_add_iff_ceilDiv_le rewrites an affine inequality in ℕ∞ using natural-number ceiling division.
• Nat.ceilDiv_mul_sub_of_lt evaluates a ceiling division after subtracting a residue smaller than the divisor.
• Nat.sum_range_sub_ceilDiv is Hermite's identity in ceiling-division form: ∑ i ∈ Finset.range n, (r - i) ⌈/⌉ n = r.

theorem ENat.natCast_le_nsmul_add_iff_ceilDiv_le {e : ℕ} (he : 0 < e) (r i : ℕ) (a : ℕ∞) : ↑r ≤ e • a + ↑i ↔ ↑((r - i) ⌈/⌉ e) ≤ a

For 0 < e, the bound r ≤ e • a + i on an extended natural number a is the bound ceil((r - i) / e) ≤ a.

theorem Nat.ceilDiv_mul_sub_of_lt {e i : ℕ} (hi : i < e) (ρ : ℕ) : (e * ρ - i) ⌈/⌉ e = ρ

For i < e, rounding (e * ρ - i) / e up gives back ρ.

theorem Nat.sum_range_sub_ceilDiv (r : ℕ) {n : ℕ} (hn : 0 < n) : ∑ i ∈ Finset.range n, (r - i) ⌈/⌉ n = r

Hermite's identity in truncated ceiling-division form: for 0 < n, the ceilings of (r - i) / n over a complete block 0 ≤ i < n of shifts add up to r. The subtraction is truncated, so the terms with r ≤ i vanish. Compare the floor form Int.sum_range_add_ediv.