Roots of natural numbers, rounded up and down

This file defines the flooring and ceiling root of a natural number. Nat.floorRoot n a/Nat.ceilRoot n a, the n-th flooring/ceiling root of a, is the natural number whose p-adic valuation is the floor/ceil of the p-adic valuation of a.

For example the 2-nd flooring and ceiling roots of 2^3 * 3^2 * 5 are 2 * 3 and 2^2 * 3 * 5 respectively. Note this is not the n-th root of a as a real number, rounded up or down.

These operations are respectively the right and left adjoints to the map a ↦ a ^ n where ℕ is ordered by divisibility. This is useful because it lets us characterise the numbers a whose n-th power divide n as the divisors of some fixed number (aka floorRoot n b). See Nat.pow_dvd_iff_dvd_floorRoot. Similarly, it lets us characterise the b whose n-th power is a multiple of a as the multiples of some fixed number (aka ceilRoot n a). See Nat.dvd_pow_iff_ceilRoot_dvd.

TODO

• norm_num extension

def Nat.floorRoot (n a : ℕ) : ℕ

Flooring root of a natural number. This divides the valuation of every prime number rounding down.

Eg if n = 2, a = 2^3 * 3^2 * 5, then floorRoot n a = 2 * 3.

In order theory terms, this is the upper or right adjoint of the map a ↦ a ^ n : ℕ → ℕ where ℕ is ordered by divisibility.

To ensure that the adjunction (Nat.pow_dvd_iff_dvd_floorRoot) holds in as many cases as possible, we special-case the following values:

• floorRoot 0 a = 0
• floorRoot n 0 = 0

Equations

• n.floorRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) => p ^ (k / n)

theorem Nat.floorRoot_def {a n : ℕ} : n.floorRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌊/⌋ n).prod fun (x1 x2 : ℕ) => x1 ^ x2

The RHS is a noncomputable version of Nat.floorRoot with better order theoretical properties.

@[simp]

theorem Nat.floorRoot_zero_left (a : ℕ) : floorRoot 0 a = 0

@[simp]

theorem Nat.floorRoot_zero_right (n : ℕ) : n.floorRoot 0 = 0

@[simp]

theorem Nat.floorRoot_one_left (a : ℕ) : floorRoot 1 a = a

@[simp]

theorem Nat.floorRoot_one_right {n : ℕ} (hn : n ≠ 0) : n.floorRoot 1 = 1

@[simp]

theorem Nat.floorRoot_pow_self {n : ℕ} (hn : n ≠ 0) (a : ℕ) : n.floorRoot (a ^ n) = a

theorem Nat.floorRoot_ne_zero {a n : ℕ} : n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

@[simp]

theorem Nat.floorRoot_eq_zero {a n : ℕ} : n.floorRoot a = 0 ↔ n = 0 ∨ a = 0

@[simp]

theorem Nat.factorization_floorRoot (n a : ℕ) : (n.floorRoot a).factorization = a.factorization ⌊/⌋ n

theorem Nat.pow_dvd_iff_dvd_floorRoot {a b n : ℕ} : a ^ n ∣ b ↔ a ∣ n.floorRoot b

Galois connection between a ↦ a ^ n : ℕ → ℕ and floorRoot n : ℕ → ℕ where ℕ is ordered by divisibility.

theorem Nat.floorRoot_pow_dvd {a n : ℕ} : n.floorRoot a ^ n ∣ a

def Nat.ceilRoot (n a : ℕ) : ℕ

Ceiling root of a natural number. This divides the valuation of every prime number rounding up.

Eg if n = 3, a = 2^4 * 3^2 * 5, then ceilRoot n a = 2^2 * 3 * 5.

In order theory terms, this is the lower or left adjoint of the map a ↦ a ^ n : ℕ → ℕ where ℕ is ordered by divisibility.

To ensure that the adjunction (Nat.dvd_pow_iff_ceilRoot_dvd) holds in as many cases as possible, we special-case the following values:

• ceilRoot 0 a = 0 (this one is not strictly necessary)
• ceilRoot n 0 = 0

Equations

• n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) => p ^ ((k + n - 1) / n)

theorem Nat.ceilRoot_def {a n : ℕ} : n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else (a.factorization ⌈/⌉ n).prod fun (x1 x2 : ℕ) => x1 ^ x2

The RHS is a noncomputable version of Nat.ceilRoot with better order theoretical properties.

@[simp]

theorem Nat.ceilRoot_zero_left (a : ℕ) : ceilRoot 0 a = 0

@[simp]

theorem Nat.ceilRoot_zero_right (n : ℕ) : n.ceilRoot 0 = 0

@[simp]

theorem Nat.ceilRoot_one_left (a : ℕ) : ceilRoot 1 a = a

@[simp]

theorem Nat.ceilRoot_one_right {n : ℕ} (hn : n ≠ 0) : n.ceilRoot 1 = 1

@[simp]

theorem Nat.ceilRoot_pow_self {n : ℕ} (hn : n ≠ 0) (a : ℕ) : n.ceilRoot (a ^ n) = a

theorem Nat.ceilRoot_ne_zero {a n : ℕ} : n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0

@[simp]

theorem Nat.ceilRoot_eq_zero {a n : ℕ} : n.ceilRoot a = 0 ↔ n = 0 ∨ a = 0

@[simp]

theorem Nat.factorization_ceilRoot (n a : ℕ) : (n.ceilRoot a).factorization = a.factorization ⌈/⌉ n

theorem Nat.dvd_pow_iff_ceilRoot_dvd {a b n : ℕ} (hn : n ≠ 0) : a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Galois connection between ceilRoot n : ℕ → ℕ and a ↦ a ^ n : ℕ → ℕ where ℕ is ordered by divisibility.

Note that this cannot possibly hold for n = 0, regardless of the value of ceilRoot 0 a, because the statement reduces to a = 1 ↔ ceilRoot 0 a ∣ b, which is false for eg a = 0, b = ceilRoot 0 a.

theorem Nat.dvd_ceilRoot_pow {a n : ℕ} (hn : n ≠ 0) : a ∣ n.ceilRoot a ^ n