Documentation

Mathlib.Data.Nat.Factorization.Root

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 #

source
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:

Equations
  • n.floorRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) => p ^ (k / n)
Instances For
    source
    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.

    source
    @[simp]
    theorem Nat.floorRoot_zero_left (a : ℕ) :
    Nat.floorRoot 0 a = 0
    source
    @[simp]
    theorem Nat.floorRoot_zero_right (n : ℕ) :
    n.floorRoot 0 = 0
    source
    @[simp]
    theorem Nat.floorRoot_one_left (a : ℕ) :
    Nat.floorRoot 1 a = a
    source
    @[simp]
    theorem Nat.floorRoot_one_right {n : ℕ} (hn : n ≠ 0) :
    n.floorRoot 1 = 1
    source
    @[simp]
    theorem Nat.floorRoot_pow_self {n : ℕ} (hn : n ≠ 0) (a : ℕ) :
    n.floorRoot (a ^ n) = a
    source
    theorem Nat.floorRoot_ne_zero {a : ℕ} {n : ℕ} :
    n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
    source
    @[simp]
    theorem Nat.floorRoot_eq_zero {a : ℕ} {n : ℕ} :
    n.floorRoot a = 0 ↔ n = 0 ∨ a = 0
    source
    @[simp]
    theorem Nat.factorization_floorRoot (n : ℕ) (a : ℕ) :
    (n.floorRoot a).factorization = a.factorization ⌊/⌋ n
    source
    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.

    source
    theorem Nat.floorRoot_pow_dvd {a : ℕ} {n : ℕ} :
    n.floorRoot a ^ n ∣ a
    source
    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:

    Equations
    • n.ceilRoot a = if n = 0 ∨ a = 0 then 0 else a.factorization.prod fun (p k : ℕ) => p ^ ((k + n - 1) / n)
    Instances For
      source
      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.

      source
      @[simp]
      theorem Nat.ceilRoot_zero_left (a : ℕ) :
      Nat.ceilRoot 0 a = 0
      source
      @[simp]
      theorem Nat.ceilRoot_zero_right (n : ℕ) :
      n.ceilRoot 0 = 0
      source
      @[simp]
      theorem Nat.ceilRoot_one_left (a : ℕ) :
      Nat.ceilRoot 1 a = a
      source
      @[simp]
      theorem Nat.ceilRoot_one_right {n : ℕ} (hn : n ≠ 0) :
      n.ceilRoot 1 = 1
      source
      @[simp]
      theorem Nat.ceilRoot_pow_self {n : ℕ} (hn : n ≠ 0) (a : ℕ) :
      n.ceilRoot (a ^ n) = a
      source
      theorem Nat.ceilRoot_ne_zero {a : ℕ} {n : ℕ} :
      n.ceilRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
      source
      @[simp]
      theorem Nat.ceilRoot_eq_zero {a : ℕ} {n : ℕ} :
      n.ceilRoot a = 0 ↔ n = 0 ∨ a = 0
      source
      @[simp]
      theorem Nat.factorization_ceilRoot (n : ℕ) (a : ℕ) :
      (n.ceilRoot a).factorization = a.factorization ⌈/⌉ n
      source
      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.

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