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 #

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
    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]
    @[simp]
    theorem Nat.floorRoot_zero_right (n : ) :
    n.floorRoot 0 = 0
    @[simp]
    @[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:

    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
      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]
      @[simp]
      theorem Nat.ceilRoot_zero_right (n : ) :
      n.ceilRoot 0 = 0
      @[simp]
      @[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