Dividing repeatedly by a power and quotient-remainder arithmetic

Facts about n / b ^ j for the stages of an argument that divides a quantity by b at each step, and exact quotient identities for division by m with remainder strictly below m.

Main results

• Nat.le_div_pow_of_mul_pow_le: lower bound on n / b ^ j when a * b ^ d ≤ n and j ≤ d.
• Nat.mul_div_pow_succ_le: b * (n / b ^ (j + 1)) ≤ n / b ^ j.
• Nat.mul_add_div_of_lt, Nat.add_mul_div_of_lt: dividing k * m + i or i + k * m by m when i < m yields k.
• Nat.mul_add_div_fin: the same for i : Fin m.
• Nat.add_sub_mod_mod_eq_ite: difference of remainders modulo d, in the form (a + d - b % d) % d.
• Nat.add_sub_mod_mod_eq_of_modEq: a modular difference is determined by its congruence.
• Nat.sum_range_mul_ite_mod: sums over < n * ℓ filtered by q % ℓ = i (for i < ℓ) equal sums of k * ℓ + i over k < n.

theorem Nat.le_div_pow_of_mul_pow_le {a b d j n : ℕ} (hb : 0 < b) (hj : j ≤ d) (h : a * b ^ d ≤ n) : a ≤ n / b ^ j

If a b ^ d ≤ n, then a ≤ n / b ^ j for every j ≤ d.

theorem Nat.mul_div_pow_succ_le (n b j : ℕ) : b * (n / b ^ (j + 1)) ≤ n / b ^ j

Dividing by one more power of b: b (n / b ^ (j + 1)) ≤ n / b ^ j.

theorem Nat.mul_add_div_of_lt (k : ℕ) {i m : ℕ} (hi : i < m) : (k * m + i) / m = k

Dividing k * m + i by m when i < m yields k.

theorem Nat.add_mul_div_of_lt (k : ℕ) {i m : ℕ} (hi : i < m) : (i + k * m) / m = k

Dividing i + k * m by m when i < m yields k.

theorem Nat.mul_add_div_fin (k : ℕ) {m : ℕ} (i : Fin m) : (k * m + ↑i) / m = k

Dividing k * m + i by m for i : Fin m yields k.

theorem Nat.add_sub_mod_mod_eq_ite (a b d : ℕ) (hd : 0 < d) : (a + d - b % d) % d = if a % d < b % d then a % d + d - b % d else a % d - b % d

Difference of remainders modulo d, in the form (a + d - b % d) % d.

theorem Nat.add_sub_mod_mod_eq_of_modEq {a b c d : ℕ} (hd : 0 < d) (hc : c < d) (he : c + b ≡ a [MOD d]) : (a + d - b % d) % d = c

A modular difference is determined by the congruence it satisfies.

theorem Nat.sum_range_mul_ite_mod {M : Type u_1} [AddCommMonoid M] (n : ℕ) {i ℓ : ℕ} (hi : i < ℓ) (F : ℕ → M) : (∑ q ∈ Finset.range (n * ℓ), if q % ℓ = i then F q else 0) = ∑ k ∈ Finset.range n, F (k * ℓ + i)

Sums over the positions of n blocks of length ℓ whose position within the block is i, as sums over the blocks.