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
Instances For
    source
    theorem Nat.floorRoot_def {a : ℕ} {n : ℕ} :
    Nat.floorRoot n a = if n = 0 ∨ a = 0 then 0 else Finsupp.prod (Nat.factorization a ⌊/⌋ n) fun (x x_1 : ℕ) => x ^ x_1

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

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

    source
    theorem Nat.floorRoot_pow_dvd {a : ℕ} {n : ℕ} :
    Nat.floorRoot n 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
    Instances For
      source
      theorem Nat.ceilRoot_def {a : ℕ} {n : ℕ} :
      Nat.ceilRoot n a = if n = 0 ∨ a = 0 then 0 else Finsupp.prod (Nat.factorization a ⌈/⌉ n) fun (x x_1 : ℕ) => x ^ x_1

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