The maximal power of one natural number dividing another

Here we introduce p.maxPowDvd n which returns the maximal k : ℕ for which p ^ k ∣ n with the convention that maxPowDvd 1 n = 0 for all n.

We prove enough about maxPowDvd in this file to show equality with Nat.padicValNat in padicValNat.padicValNat_eq_maxPowDvd.

The implementation of maxPowDvd improves on the speed of padicValNat.

def Nat.maxPowDvdDiv (p n : ℕ) : ℕ × ℕ

Find largest k : ℕ such that p ^ k ∣ n for any p : ℕ, as well as the ratio n / p ^ k.

The implementation recurses from (p, n) to (p * p, n), so the recursion depth is $$O(\log(\nu_p(n)))$$, thus it is $$O(\log(\log(n)))$$.

@[irreducible]

def Nat.maxPowDvdDiv.go (n p : ℕ) (hp : 1 < p ∧ n ≠ 0) : ℕ × ℕ

Auxiliary definition for Nat.maxPowDvdDiv.

def Nat.divMaxPow (n p : ℕ) : ℕ

Divide n by the maximal power of p that divides n.

theorem Nat.maxPowDvdDiv.go_spec {n p : ℕ} (hnp : 1 < p ∧ n ≠ 0) : (go n p hnp).snd * p ^ (go n p hnp).fst = n ∧ ¬p ∣ (go n p hnp).snd

theorem Nat.maxPowDvdDiv_of_base_le_one {p : ℕ} (hp : p ≤ 1) (n : ℕ) : p.maxPowDvdDiv n = (0, n)

@[simp]

theorem Nat.maxPowDvdDiv_zero_left (n : ℕ) : maxPowDvdDiv 0 n = (0, n)

@[simp]

theorem Nat.divMaxPow_zero_right (n : ℕ) : n.divMaxPow 0 = n

@[simp]

theorem Nat.maxPowDvdDiv_one_left (n : ℕ) : maxPowDvdDiv 1 n = (0, n)

@[simp]

theorem Nat.divMaxPow_one_right (n : ℕ) : n.divMaxPow 1 = n

@[simp]

theorem Nat.maxPowDvdDiv_zero_right (p : ℕ) : p.maxPowDvdDiv 0 = (0, 0)

@[simp]

theorem Nat.divMaxPow_zero_left (p : ℕ) : divMaxPow 0 p = 0

theorem Nat.not_dvd_divMaxPow {p n : ℕ} (hp : 1 < p) (hn : n ≠ 0) : ¬p ∣ n.divMaxPow p