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
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
- Nat.floorRoot n a = if n = 0 ∨ a = 0 then 0 else Finsupp.prod (Nat.factorization a) fun (p k : ℕ) => p ^ (k / n)
Instances For
The RHS is a noncomputable version of Nat.floorRoot
with better order theoretical
properties.
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
- Nat.ceilRoot n a = if n = 0 ∨ a = 0 then 0 else Finsupp.prod (Nat.factorization a) fun (p k : ℕ) => p ^ ((k + n - 1) / n)
Instances For
The RHS is a noncomputable version of Nat.ceilRoot
with better order theoretical
properties.
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
.