p-adic Valuation

This file defines the p-adic valuation on ℕ, ℤ, and ℚ.

The p-adic valuation on ℚ is the difference of the multiplicities of p in the numerator and denominator of q. This function obeys the standard properties of a valuation, with the appropriate assumptions on p. The p-adic valuations on ℕ and ℤ agree with that on ℚ.

The valuation induces a norm on ℚ. This norm is defined in padicNorm.lean.

Notations

This file uses the local notation /. for Rat.mk.

Implementation notes

Much, but not all, of this file assumes that p is prime. This assumption is inferred automatically by taking [Fact p.Prime] as a type class argument.

Calculations with p-adic valuations

• padicValNat_factorial: Legendre's Theorem. The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n. See Nat.Prime.multiplicity_factorial for the same result but stated in the language of prime multiplicity.

• sub_one_mul_padicValNat_factorial_eq_sub_sum_digits: Legendre's Theorem. Taking (p - 1) times the p-adic valuation of n! equals n minus the sum of base p digits of n.

• padicValNat_choose: Kummer's Theorem. The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n. See Nat.Prime.multiplicity_choose for the same result but stated in the language of prime multiplicity.

• sub_one_mul_padicValNat_choose_eq_sub_sum_digits: Kummer's Theorem. Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

References

• [F. Q. Gouvêa, p-adic numbers][gouvea1997]
• [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
• https://en.wikipedia.org/wiki/P-adic_number

Tags

p-adic, p adic, padic, norm, valuation

def padicValNat (p : ℕ) (n : ℕ) : ℕ

For p ≠ 1, the p-adic valuation of a natural n ≠ 0 is the largest natural number k such that p^k divides z. If n = 0 or p = 1, then padicValNat p q defaults to 0.

Equations

• padicValNat p n = if h : p ≠ 1 ∧ 0 < n then Part.get (multiplicity p n) (_ : multiplicity.Finite p n) else 0

@[simp]

theorem padicValNat.zero {p : ℕ} : padicValNat p 0 = 0

padicValNat p 0 is 0 for any p.

@[simp]

theorem padicValNat.one {p : ℕ} : padicValNat p 1 = 0

padicValNat p 1 is 0 for any p.

@[simp]

theorem padicValNat.self {p : ℕ} (hp : 1 < p) : padicValNat p p = 1

If p ≠ 0 and p ≠ 1, then padicValNat p p is 1.

@[simp]

theorem padicValNat.eq_zero_iff {p : ℕ} {n : ℕ} : padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

theorem padicValNat.eq_zero_of_not_dvd {p : ℕ} {n : ℕ} (h : ¬p ∣ n) : padicValNat p n = 0

theorem padicValNat.maxPowDiv_eq_multiplicity {p : ℕ} {n : ℕ} (hp : 1 < p) (hn : 0 < n) : ↑(Nat.maxPowDiv p n) = multiplicity p n

theorem padicValNat.maxPowDiv_eq_multiplicity_get {p : ℕ} {n : ℕ} (hp : 1 < p) (hn : 0 < n) (h : multiplicity.Finite p n) : Nat.maxPowDiv p n = Part.get (multiplicity p n) h

@[csimp]

theorem padicValNat.padicValNat_eq_maxPowDiv : padicValNat = Nat.maxPowDiv

Allows for more efficient code for padicValNat

def padicValInt (p : ℕ) (z : ℤ) : ℕ

For p ≠ 1, the p-adic valuation of an integer z ≠ 0 is the largest natural number k such that p^k divides z. If x = 0 or p = 1, then padicValInt p q defaults to 0.

Equations

• padicValInt p z = padicValNat p (Int.natAbs z)

theorem padicValInt.of_ne_one_ne_zero {p : ℕ} {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padicValInt p z = Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z)

@[simp]

theorem padicValInt.zero {p : ℕ} : padicValInt p 0 = 0

padicValInt p 0 is 0 for any p.

@[simp]

theorem padicValInt.one {p : ℕ} : padicValInt p 1 = 0

padicValInt p 1 is 0 for any p.

@[simp]

theorem padicValInt.of_nat {p : ℕ} {n : ℕ} : padicValInt p ↑n = padicValNat p n

The p-adic value of a natural is its p-adic value as an integer.

theorem padicValInt.self {p : ℕ} (hp : 1 < p) : padicValInt p ↑p = 1

If p ≠ 0 and p ≠ 1, then padicValInt p p is 1.

theorem padicValInt.eq_zero_of_not_dvd {p : ℕ} {z : ℤ} (h : ¬↑p ∣ z) : padicValInt p z = 0

def padicValRat (p : ℕ) (q : ℚ) : ℤ

padicValRat defines the valuation of a rational q to be the valuation of q.num minus the valuation of q.den. If q = 0 or p = 1, then padicValRat p q defaults to 0.

Equations

• padicValRat p q = ↑(padicValInt p q.num) - ↑(padicValNat p q.den)

theorem padicValRat_def (p : ℕ) (q : ℚ) : padicValRat p q = ↑(padicValInt p q.num) - ↑(padicValNat p q.den)

@[simp]

theorem padicValRat.neg {p : ℕ} (q : ℚ) : padicValRat p (-q) = padicValRat p q

padicValRat p q is symmetric in q.

@[simp]

theorem padicValRat.zero {p : ℕ} : padicValRat p 0 = 0

padicValRat p 0 is 0 for any p.

@[simp]

theorem padicValRat.one {p : ℕ} : padicValRat p 1 = 0

padicValRat p 1 is 0 for any p.

@[simp]

theorem padicValRat.of_int {p : ℕ} {z : ℤ} : padicValRat p ↑z = ↑(padicValInt p z)

The p-adic value of an integer z ≠ 0 is its p-adic_value as a rational.

theorem padicValRat.of_int_multiplicity {p : ℕ} {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) : padicValRat p ↑z = ↑(Part.get (multiplicity (↑p) z) (_ : multiplicity.Finite (↑p) z))

The p-adic value of an integer z ≠ 0 is the multiplicity of p in z.

theorem padicValRat.multiplicity_sub_multiplicity {p : ℕ} {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) : padicValRat p q = ↑(Part.get (multiplicity (↑p) q.num) (_ : multiplicity.Finite (↑p) q.num)) - ↑(Part.get (multiplicity p q.den) (_ : (multiplicity p q.den).Dom))

@[simp]

theorem padicValRat.of_nat {p : ℕ} {n : ℕ} : padicValRat p ↑n = ↑(padicValNat p n)

The p-adic value of an integer z ≠ 0 is its p-adic value as a rational.

theorem padicValRat.self {p : ℕ} (hp : 1 < p) : padicValRat p ↑p = 1

If p ≠ 0 and p ≠ 1, then padicValRat p p is 1.

theorem zero_le_padicValRat_of_nat {p : ℕ} (n : ℕ) : 0 ≤ padicValRat p ↑n

theorem padicValRat_of_nat {p : ℕ} (n : ℕ) : ↑(padicValNat p n) = padicValRat p ↑n

padicValRat coincides with padicValNat.

theorem padicValNat_def {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 0 < n) : padicValNat p n = Part.get (multiplicity p n) (_ : multiplicity.Finite p n)

A simplification of padicValNat when one input is prime, by analogy with padicValRat_def.

theorem padicValNat_def' {p : ℕ} {n : ℕ} (hp : p ≠ 1) (hn : 0 < n) : ↑(padicValNat p n) = multiplicity p n

@[simp]

theorem padicValNat_self {p : ℕ} [Fact (Nat.Prime p)] : padicValNat p p = 1

theorem one_le_padicValNat_of_dvd {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] (hn : 0 < n) (div : p ∣ n) : 1 ≤ padicValNat p n

theorem dvd_iff_padicValNat_ne_zero {p : ℕ} {n : ℕ} [Fact (Nat.Prime p)] (hn0 : n ≠ 0) : p ∣ n ↔ padicValNat p n ≠ 0

theorem padicValRat.finite_int_prime_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ} : multiplicity.Finite (↑p) a ↔ a ≠ 0

The multiplicity of p : ℕ in a : ℤ is finite exactly when a ≠ 0.

theorem padicValRat.defn (p : ℕ) [hp : Fact (Nat.Prime p)] {q : ℚ} {n : ℤ} {d : ℤ} (hqz : q ≠ 0) (qdf : q = Rat.divInt n d) : padicValRat p q = ↑(Part.get (multiplicity (↑p) n) (_ : multiplicity.Finite (↑p) n)) - ↑(Part.get (multiplicity (↑p) d) (_ : multiplicity.Finite (↑p) d))

A rewrite lemma for padicValRat p q when q is expressed in terms of Rat.mk.

theorem padicValRat.mul {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) : padicValRat p (q * r) = padicValRat p q + padicValRat p r

A rewrite lemma for padicValRat p (q * r) with conditions q ≠ 0, r ≠ 0.

theorem padicValRat.pow {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} (hq : q ≠ 0) {k : ℕ} : padicValRat p (q ^ k) = ↑k * padicValRat p q

A rewrite lemma for padicValRat p (q^k) with condition q ≠ 0.

theorem padicValRat.inv {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ) : padicValRat p q⁻¹ = -padicValRat p q

A rewrite lemma for padicValRat p (q⁻¹) with condition q ≠ 0.

theorem padicValRat.div {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) : padicValRat p (q / r) = padicValRat p q - padicValRat p r

A rewrite lemma for padicValRat p (q / r) with conditions q ≠ 0, r ≠ 0.

theorem padicValRat.padicValRat_le_padicValRat_iff {p : ℕ} [hp : Fact (Nat.Prime p)] {n₁ : ℤ} {n₂ : ℤ} {d₁ : ℤ} {d₂ : ℤ} (hn₁ : n₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) : padicValRat p (Rat.divInt n₁ d₁) ≤ padicValRat p (Rat.divInt n₂ d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

A condition for padicValRat p (n₁ / d₁) ≤ padicValRat p (n₂ / d₂), in terms of divisibility by p^n.

theorem padicValRat.le_padicValRat_add_of_le {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r : ℚ} (hqr : q + r ≠ 0) (h : padicValRat p q ≤ padicValRat p r) : padicValRat p q ≤ padicValRat p (q + r)

Sufficient conditions to show that the p-adic valuation of q is less than or equal to the p-adic valuation of q + r.

theorem padicValRat.min_le_padicValRat_add {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r : ℚ} (hqr : q + r ≠ 0) : min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r)

The minimum of the valuations of q and r is at most the valuation of q + r.

theorem padicValRat.add_eq_min {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q ≠ padicValRat p r) : padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r)

Ultrametric property of a p-adic valuation.

theorem padicValRat.add_eq_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q < padicValRat p r) : padicValRat p (q + r) = padicValRat p q

theorem padicValRat.lt_add_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} {r₁ : ℚ} {r₂ : ℚ} (hqr : r₁ + r₂ ≠ 0) (hval₁ : padicValRat p q < padicValRat p r₁) (hval₂ : padicValRat p q < padicValRat p r₂) : padicValRat p q < padicValRat p (r₁ + r₂)

@[simp]

theorem padicValRat.self_pow_inv {p : ℕ} [hp : Fact (Nat.Prime p)] (r : ℕ) : padicValRat p (↑p ^ r)⁻¹ = -↑r

theorem padicValRat.sum_pos_of_pos {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {F : ℕ → ℚ} (hF : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)) (hn0 : (Finset.sum (Finset.range n) fun i => F i) ≠ 0) : 0 < padicValRat p (Finset.sum (Finset.range n) fun i => F i)

A finite sum of rationals with positive p-adic valuation has positive p-adic valuation (if the sum is non-zero).

theorem padicValRat.lt_sum_of_lt {p : ℕ} {j : ℕ} [hp : Fact (Nat.Prime p)] {F : ℕ → ℚ} {S : Finset ℕ} (hS : Finset.Nonempty S) (hF : ∀ (i : ℕ), i ∈ S → padicValRat p (F j) < padicValRat p (F i)) (hn1 : ∀ (i : ℕ), 0 < F i) : padicValRat p (F j) < padicValRat p (Finset.sum S fun i => F i)

If the p-adic valuation of a finite set of positive rationals is greater than a given rational number, then the p-adic valuation of their sum is also greater than the same rational number.

theorem padicValNat.mul {p : ℕ} {a : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] : a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b

A rewrite lemma for padicValNat p (a * b) with conditions a ≠ 0, b ≠ 0.

theorem padicValNat.div_of_dvd {p : ℕ} {a : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] (h : b ∣ a) : padicValNat p (a / b) = padicValNat p a - padicValNat p b

theorem padicValNat.div {p : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] (dvd : p ∣ b) : padicValNat p (b / p) = padicValNat p b - 1

Dividing out by a prime factor reduces the padicValNat by 1.

theorem padicValNat.pow {p : ℕ} {a : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (ha : a ≠ 0) : padicValNat p (a ^ n) = n * padicValNat p a

A version of padicValRat.pow for padicValNat.

@[simp]

theorem padicValNat.prime_pow {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : padicValNat p (p ^ n) = n

theorem padicValNat.div_pow {p : ℕ} {a : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] (dvd : p ^ a ∣ b) : padicValNat p (b / p ^ a) = padicValNat p b - a

theorem padicValNat.div' {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (cpm : Nat.Coprime p m) {b : ℕ} (dvd : m ∣ b) : padicValNat p (b / m) = padicValNat p b

theorem dvd_of_one_le_padicValNat {p : ℕ} {n : ℕ} (hp : 1 ≤ padicValNat p n) : p ∣ n

theorem pow_padicValNat_dvd {p : ℕ} {n : ℕ} : p ^ padicValNat p n ∣ n

theorem padicValNat_dvd_iff_le {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℕ} {n : ℕ} (ha : a ≠ 0) : p ^ n ∣ a ↔ n ≤ padicValNat p a

theorem padicValNat_dvd_iff {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] (a : ℕ) : p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a

theorem pow_succ_padicValNat_not_dvd {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] (hn : n ≠ 0) : ¬p ^ (padicValNat p n + 1) ∣ n

theorem padicValNat_primes {p : ℕ} {q : ℕ} [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (neq : p ≠ q) : padicValNat p q = 0

theorem padicValNat_le_nat_log {p : ℕ} (n : ℕ) : padicValNat p n ≤ Nat.log p n

The p-adic valuation of n is less than or equal to its logarithm w.r.t p.

theorem nat_log_eq_padicValNat_iff {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] (hn : 0 < n) : Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)

The p-adic valuation of n is equal to the logarithm w.r.t p iff n is less than p raised to one plus the p-adic valuation of n.

theorem Nat.log_ne_padicValNat_succ {n : ℕ} (hn : n ≠ 0) : Nat.log 2 n ≠ padicValNat 2 (n + 1)

theorem Nat.max_log_padicValNat_succ_eq_log_succ (n : ℕ) : max (Nat.log 2 n) (padicValNat 2 (n + 1)) = Nat.log 2 (n + 1)

theorem range_pow_padicValNat_subset_divisors {p : ℕ} {n : ℕ} (hn : n ≠ 0) : Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ Nat.divisors n

theorem range_pow_padicValNat_subset_divisors' {p : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] : Finset.image (fun t => p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ Finset.erase (Nat.divisors n) 1

theorem padicValNat_factorial_mul {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] : padicValNat p (Nat.factorial (p * n)) = padicValNat p (Nat.factorial n) + n

The p-adic valuation of (p * n)! is n more than that of n!.

theorem padicValNat_eq_zero_of_mem_Ioo {p : ℕ} {m : ℕ} {k : ℕ} (hm : m ∈ Set.Ioo (p * k) (p * (k + 1))) : padicValNat p m = 0

The p-adic valuation of m equals zero if it is between p * k and p * (k + 1) for some k.

theorem padicValNat_factorial_mul_add {p : ℕ} {n : ℕ} (m : ℕ) [hp : Fact (Nat.Prime p)] (h : n < p) : padicValNat p (Nat.factorial (p * m + n)) = padicValNat p (Nat.factorial (p * m))

@[simp]

theorem padicValNat_mul_div_factorial {p : ℕ} (n : ℕ) [hp : Fact (Nat.Prime p)] : padicValNat p (Nat.factorial (p * (n / p))) = padicValNat p (Nat.factorial n)

The p-adic valuation of n! is equal to the p-adic valuation of the factorial of the largest multiple of p below n, i.e. (p * ⌊n / p⌋)!.

theorem padicValNat_factorial {p : ℕ} {n : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p n < b) : padicValNat p (Nat.factorial n) = Finset.sum (Finset.Ico 1 b) fun i => n / p ^ i

Legendre's Theorem

The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

theorem sub_one_mul_padicValNat_factorial_eq_sub_sum_digits {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) : (p - 1) * padicValNat p (Nat.factorial n) = n - List.sum (Nat.digits p n)

Legendre's Theorem

Taking (p - 1) times the p-adic valuation of n! equals n minus the sum of base p digits of n.

theorem padicValNat_choose {p : ℕ} {n : ℕ} {k : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] (hkn : k ≤ n) (hnb : Nat.log p n < b) : padicValNat p (Nat.choose n k) = Finset.card (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b))

Kummer's Theorem

The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

theorem padicValNat_choose' {p : ℕ} {n : ℕ} {k : ℕ} {b : ℕ} [hp : Fact (Nat.Prime p)] (hnb : Nat.log p (n + k) < b) : padicValNat p (Nat.choose (n + k) k) = Finset.card (Finset.filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b))

Kummer's Theorem

The p-adic valuation of (n + k).choose k is the number of carries when k and n are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p (n + k).

theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' {p : ℕ} {k : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] : (p - 1) * padicValNat p (Nat.choose (n + k) k) = List.sum (Nat.digits p k) + List.sum (Nat.digits p n) - List.sum (Nat.digits p (n + k))

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n + k over k equals the sum of the digits of k plus the sum of the digits of n minus the sum of digits of n + k, all base p.

theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {p : ℕ} {k : ℕ} {n : ℕ} [hp : Fact (Nat.Prime p)] (h : k ≤ n) : (p - 1) * padicValNat p (Nat.choose n k) = List.sum (Nat.digits p k) + List.sum (Nat.digits p (n - k)) - List.sum (Nat.digits p n)

Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

theorem padicValInt_dvd_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ) (a : ℤ) : ↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a

theorem padicValInt_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ) : ↑p ^ padicValInt p a ∣ a

theorem padicValInt_self {p : ℕ} [hp : Fact (Nat.Prime p)] : padicValInt p ↑p = 1

theorem padicValInt.mul {p : ℕ} [hp : Fact (Nat.Prime p)] {a : ℤ} {b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : padicValInt p (a * b) = padicValInt p a + padicValInt p b

theorem padicValInt_mul_eq_succ {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℤ) (ha : a ≠ 0) : padicValInt p (a * ↑p) = padicValInt p a + 1