mathlib documentation

number_theory.padics.padic_norm

p-adic norm #

This file defines the p-adic valuation and the p-adic norm on ℚ.

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 valuation induces a norm on ℚ. This norm is a nonarchimedean absolute value. It takes values in {0} ∪ {1/p^k | k ∈ ℤ}.

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 (prime p)] as a type class argument.

References #

Tags #

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

source
def padic_val_nat (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 padic_val_nat p q defaults to 0.

Equations
source
@[protected, simp]
theorem padic_val_nat.zero {p : ℕ} :
padic_val_nat p 0 = 0

padic_val_nat p 0 is 0 for any p.

source
@[protected, simp]
theorem padic_val_nat.one {p : ℕ} :
padic_val_nat p 1 = 0

padic_val_nat p 1 is 0 for any p.

source
@[simp]
theorem padic_val_nat.self {p : ℕ} (hp : 1 < p) :
padic_val_nat p p = 1

For p ≠ 0, p ≠ 1,padic_val_rat p p` is 1.

source
theorem padic_val_nat.eq_zero_of_not_dvd {p n : ℕ} (h : ¬p ∣ n) :
padic_val_nat p n = 0
source
def padic_val_int (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 padic_val_int p q defaults to 0.

Equations
source
theorem padic_val_int.of_ne_one_ne_zero {p : ℕ} {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) :
padic_val_int p z = (multiplicity ↑p z).get _
source
@[protected, simp]
theorem padic_val_int.zero {p : ℕ} :
padic_val_int p 0 = 0

padic_val_int p 0 is 0 for any p.

source
@[protected, simp]
theorem padic_val_int.one {p : ℕ} :
padic_val_int p 1 = 0

padic_val_int p 1 is 0 for any p.

source
@[simp]
theorem padic_val_int.of_nat {p n : ℕ} :
padic_val_int p ↑n = padic_val_nat p n

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

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

For p ≠ 0, p ≠ 1,padic_val_int p p` is 1.

source
theorem padic_val_int.eq_zero_of_not_dvd {p : ℕ} {z : ℤ} (h : ¬↑p ∣ z) :
padic_val_int p z = 0
source
def padic_val_rat (p : ℕ) (q : ℚ) :
ℤ

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

Equations
source
@[protected, simp]
theorem padic_val_rat.neg {p : ℕ} (q : ℚ) :
padic_val_rat p (-q) = padic_val_rat p q

padic_val_rat p q is symmetric in q.

source
@[protected, simp]
theorem padic_val_rat.zero (m : ℕ) :
padic_val_rat m 0 = 0

padic_val_rat p 0 is 0 for any p.

source
@[protected, simp]
theorem padic_val_rat.one {p : ℕ} :
padic_val_rat p 1 = 0

padic_val_rat p 1 is 0 for any p.

source
@[simp]
theorem padic_val_rat.of_int {p : ℕ} {z : ℤ} :
padic_val_rat p ↑z = ↑(padic_val_int p z)

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

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

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

source
theorem padic_val_rat.multiplicity_sub_multiplicity {p : ℕ} {q : ℚ} (hp : p ≠ 1) (hq : q ≠ 0) :
padic_val_rat p q = ↑((multiplicity ↑p q.num).get _) - ↑((multiplicity p q.denom).get _)
source
@[simp]
theorem padic_val_rat.of_nat {p n : ℕ} :
padic_val_rat p ↑n = ↑(padic_val_nat p n)

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

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

For p ≠ 0, p ≠ 1,padic_val_rat p p` is 1.

source
theorem zero_le_padic_val_rat_of_nat (p n : ℕ) :
0 ≤ padic_val_rat p ↑n
source
@[norm_cast]
theorem padic_val_rat_of_nat (p n : ℕ) :
↑(padic_val_nat p n) = padic_val_rat p ↑n
source
theorem padic_val_nat_def {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} (hn : 0 < n) :
padic_val_nat p n = (multiplicity p n).get _

A simplification of padic_val_nat when one input is prime, by analogy with padic_val_rat_def.

source
@[simp]
theorem padic_val_nat_self (p : ℕ) [fact (nat.prime p)] :
padic_val_nat p p = 1
source
theorem one_le_padic_val_nat_of_dvd {n p : ℕ} [prime : fact (nat.prime p)] (n_pos : 0 < n) (div : p ∣ n) :
1 ≤ padic_val_nat p n
source
theorem padic_val_rat.finite_int_prime_iff {p : ℕ} [p_prime : fact (nat.prime p)] {a : ℤ} :
multiplicity.finite ↑p a ↔ a ≠ 0

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

source
@[protected]
theorem padic_val_rat.defn (p : ℕ) [p_prime : fact (nat.prime p)] {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = n /. d) :
padic_val_rat p q = ↑((multiplicity ↑p n).get _) - ↑((multiplicity ↑p d).get _)

A rewrite lemma for padic_val_rat p q when q is expressed in terms of rat.mk.

source
@[protected]
theorem padic_val_rat.mul (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) :
padic_val_rat p (q * r) = padic_val_rat p q + padic_val_rat p r

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

source
@[protected]
theorem padic_val_rat.pow (p : ℕ) [p_prime : fact (nat.prime p)] {q : ℚ} (hq : q ≠ 0) {k : ℕ} :
padic_val_rat p (q ^ k) = (↑k) * padic_val_rat p q

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

source
@[protected]
theorem padic_val_rat.inv (p : ℕ) [p_prime : fact (nat.prime p)] (q : ℚ) :
padic_val_rat p q⁻¹ = -padic_val_rat p q

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

source
@[protected]
theorem padic_val_rat.div (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) :
padic_val_rat p (q / r) = padic_val_rat p q - padic_val_rat p r

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

source
theorem padic_val_rat.padic_val_rat_le_padic_val_rat_iff (p : ℕ) [p_prime : fact (nat.prime p)] {n₁ n₂ d₁ d₂ : ℤ} (hn₁ : n₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) :
padic_val_rat p (n₁ /. d₁) ≤ padic_val_rat p (n₂ /. d₂) ↔ ∀ (n : ℕ), ↑p ^ n ∣ n₁ * d₂ → ↑p ^ n ∣ n₂ * d₁

A condition for padic_val_rat p (n₁ / d₁) ≤ padic_val_rat p (n₂ / d₂), in terms of divisibility byp^n`.

source
theorem padic_val_rat.le_padic_val_rat_add_of_le (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℚ} (hqr : q + r ≠ 0) (h : padic_val_rat p q ≤ padic_val_rat p r) :
padic_val_rat p q ≤ padic_val_rat p (q + r)

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

source
theorem padic_val_rat.min_le_padic_val_rat_add (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℚ} (hqr : q + r ≠ 0) :
min (padic_val_rat p q) (padic_val_rat p r) ≤ padic_val_rat p (q + r)

The minimum of the valuations of q and r is less than or equal to the valuation of q + r.

source
theorem padic_val_rat.sum_pos_of_pos (p : ℕ) [p_prime : fact (nat.prime p)] {n : ℕ} {F : ℕ → ℚ} (hF : ∀ (i : ℕ), i < n → 0 < padic_val_rat p (F i)) (hn0 : ∑ (i : ℕ) in finset.range n, F i ≠ 0) :
0 < padic_val_rat p (∑ (i : ℕ) in finset.range n, F i)

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

source
@[protected]
theorem padic_val_nat.mul (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℕ} (hq : q ≠ 0) (hr : r ≠ 0) :
padic_val_nat p (q * r) = padic_val_nat p q + padic_val_nat p r

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

source
@[protected]
theorem padic_val_nat.div_of_dvd (p : ℕ) [hp : fact (nat.prime p)] {a b : ℕ} (h : b ∣ a) :
padic_val_nat p (a / b) = padic_val_nat p a - padic_val_nat p b
source
@[protected]
theorem padic_val_nat.div {p : ℕ} [p_prime : fact (nat.prime p)] {b : ℕ} (dvd : p ∣ b) :
padic_val_nat p (b / p) = padic_val_nat p b - 1

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

source
@[protected]
theorem padic_val_nat.pow (p q n : ℕ) [fact (nat.prime p)] (hq : q ≠ 0) :
padic_val_nat p (q ^ n) = n * padic_val_nat p q

A version of padic_val_rat.pow for padic_val_nat

source
@[protected, simp]
theorem padic_val_nat.prime_pow (p n : ℕ) [fact (nat.prime p)] :
padic_val_nat p (p ^ n) = n
source
@[protected]
theorem padic_val_nat.div_pow {p : ℕ} [p_prime : fact (nat.prime p)] {b k : ℕ} (dvd : p ^ k ∣ b) :
padic_val_nat p (b / p ^ k) = padic_val_nat p b - k
source
theorem dvd_of_one_le_padic_val_nat {n p : ℕ} (hp : 1 ≤ padic_val_nat p n) :
p ∣ n
source
theorem pow_padic_val_nat_dvd {p n : ℕ} [fact (nat.prime p)] :
p ^ padic_val_nat p n ∣ n
source
theorem pow_succ_padic_val_nat_not_dvd {p n : ℕ} [hp : fact (nat.prime p)] (hn : 0 < n) :
¬p ^ (padic_val_nat p n + 1) ∣ n
source
theorem padic_val_nat_dvd_iff (p : ℕ) [hp : fact (nat.prime p)] (n a : ℕ) :
p ^ n ∣ a ↔ a = 0 ∨ n ≤ padic_val_nat p a
source
theorem padic_val_nat_primes {p q : ℕ} [p_prime : fact (nat.prime p)] [q_prime : fact (nat.prime q)] (neq : p ≠ q) :
padic_val_nat p q = 0
source
@[protected]
theorem padic_val_nat.div' {p : ℕ} [p_prime : fact (nat.prime p)] {m : ℕ} (cpm : p.coprime m) {b : ℕ} (dvd : m ∣ b) :
padic_val_nat p (b / m) = padic_val_nat p b
source
theorem padic_val_nat_eq_factorization (p n : ℕ) [hp : fact (nat.prime p)] :
padic_val_nat p n = ⇑(n.factorization) p
source
theorem prod_pow_prime_padic_val_nat (n : ℕ) (hn : n ≠ 0) (m : ℕ) (pr : n < m) :
∏ (p : ℕ) in finset.filter nat.prime (finset.range m), p ^ padic_val_nat p n = n
source
theorem range_pow_padic_val_nat_subset_divisors {n : ℕ} (p : ℕ) [fact (nat.prime p)] (hn : n ≠ 0) :
finset.image (pow p) (finset.range (padic_val_nat p n + 1)) ⊆ n.divisors
source
theorem range_pow_padic_val_nat_subset_divisors' {n : ℕ} (p : ℕ) [h : fact (nat.prime p)] :
finset.image (λ (t : ℕ), p ^ (t + 1)) (finset.range (padic_val_nat p n)) ⊆ n.divisors \ {1}
source
theorem padic_val_int_dvd_iff (p : ℕ) [fact (nat.prime p)] (n : ℕ) (a : ℤ) :
↑p ^ n ∣ a ↔ a = 0 ∨ n ≤ padic_val_int p a
source
theorem padic_val_int_dvd (p : ℕ) [fact (nat.prime p)] (a : ℤ) :
↑p ^ padic_val_int p a ∣ a
source
theorem padic_val_int_self (p : ℕ) [pp : fact (nat.prime p)] :
padic_val_int p ↑p = 1
source
theorem padic_val_int.mul (p : ℕ) [fact (nat.prime p)] {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) :
padic_val_int p (a * b) = padic_val_int p a + padic_val_int p b
source
theorem padic_val_int_mul_eq_succ (p : ℕ) [pp : fact (nat.prime p)] (a : ℤ) (ha : a ≠ 0) :
padic_val_int p (a * ↑p) = padic_val_int p a + 1
source
def padic_norm (p : ℕ) (q : ℚ) :
ℚ

If q ≠ 0, the p-adic norm of a rational q is p ^ (-(padic_val_rat p q)). If q = 0, the p-adic norm of q is 0.

Equations
source
@[protected, simp]
theorem padic_norm.eq_zpow_of_nonzero (p : ℕ) {q : ℚ} (hq : q ≠ 0) :
padic_norm p q = ↑p ^ -padic_val_rat p q

Unfolds the definition of the p-adic norm of q when q ≠ 0.

source
@[protected]
theorem padic_norm.nonneg (p : ℕ) (q : ℚ) :
0 ≤ padic_norm p q

The p-adic norm is nonnegative.

source
@[protected, simp]
theorem padic_norm.zero (p : ℕ) :
padic_norm p 0 = 0

The p-adic norm of 0 is 0.

source
@[protected, simp]
theorem padic_norm.one (p : ℕ) :
padic_norm p 1 = 1

The p-adic norm of 1 is 1.

source
theorem padic_norm.padic_norm_p {p : ℕ} (hp : 1 < p) :
padic_norm p ↑p = 1 / ↑p

The p-adic norm of p is 1/p if p > 1.

See also padic_norm.padic_norm_p_of_prime for a version that assumes p is prime.

source
@[simp]
theorem padic_norm.padic_norm_p_of_prime (p : ℕ) [fact (nat.prime p)] :
padic_norm p ↑p = 1 / ↑p

The p-adic norm of p is 1/p if p is prime.

See also padic_norm.padic_norm_p for a version that assumes 1 < p.

source
theorem padic_norm.padic_norm_of_prime_of_ne {p q : ℕ} [p_prime : fact (nat.prime p)] [q_prime : fact (nat.prime q)] (neq : p ≠ q) :
padic_norm p ↑q = 1

The p-adic norm of q is 1 if q is prime and not equal to p.

source
theorem padic_norm.padic_norm_p_lt_one {p : ℕ} (hp : 1 < p) :
padic_norm p ↑p < 1

The p-adic norm of p is less than 1 if 1 < p.

See also padic_norm.padic_norm_p_lt_one_of_prime for a version assuming prime p.

source
theorem padic_norm.padic_norm_p_lt_one_of_prime (p : ℕ) [fact (nat.prime p)] :
padic_norm p ↑p < 1

The p-adic norm of p is less than 1 if p is prime.

See also padic_norm.padic_norm_p_lt_one for a version assuming 1 < p.

source
@[protected]
theorem padic_norm.values_discrete (p : ℕ) {q : ℚ} (hq : q ≠ 0) :
∃ (z : ℤ), padic_norm p q = ↑p ^ -z

padic_norm p q takes discrete values p ^ -z for z : ℤ.

source
@[protected, simp]
theorem padic_norm.neg (p : ℕ) (q : ℚ) :
padic_norm p (-q) = padic_norm p q

padic_norm p is symmetric.

source
@[protected]
theorem padic_norm.nonzero (p : ℕ) [hp : fact (nat.prime p)] {q : ℚ} (hq : q ≠ 0) :
padic_norm p q ≠ 0

If q ≠ 0, then padic_norm p q ≠ 0.

source
theorem padic_norm.zero_of_padic_norm_eq_zero (p : ℕ) [hp : fact (nat.prime p)] {q : ℚ} (h : padic_norm p q = 0) :
q = 0

If the p-adic norm of q is 0, then q is 0.

source
@[protected, simp]
theorem padic_norm.mul (p : ℕ) [hp : fact (nat.prime p)] (q r : ℚ) :
padic_norm p (q * r) = (padic_norm p q) * padic_norm p r

The p-adic norm is multiplicative.

source
@[protected, simp]
theorem padic_norm.div (p : ℕ) [hp : fact (nat.prime p)] (q r : ℚ) :
padic_norm p (q / r) = padic_norm p q / padic_norm p r

The p-adic norm respects division.

source
@[protected]
theorem padic_norm.of_int (p : ℕ) [hp : fact (nat.prime p)] (z : ℤ) :
padic_norm p ↑z ≤ 1

The p-adic norm of an integer is at most 1.

source
@[protected]
theorem padic_norm.nonarchimedean (p : ℕ) [hp : fact (nat.prime p)] {q r : ℚ} :
padic_norm p (q + r) ≤ max (padic_norm p q) (padic_norm p r)

The p-adic norm is nonarchimedean: the norm of p + q is at most the max of the norm of p and the norm of q.

source
theorem padic_norm.triangle_ineq (p : ℕ) [hp : fact (nat.prime p)] (q r : ℚ) :
padic_norm p (q + r) ≤ padic_norm p q + padic_norm p r

The p-adic norm respects the triangle inequality: the norm of p + q is at most the norm of p plus the norm of q.

source
@[protected]
theorem padic_norm.sub (p : ℕ) [hp : fact (nat.prime p)] {q r : ℚ} :
padic_norm p (q - r) ≤ max (padic_norm p q) (padic_norm p r)

The p-adic norm of a difference is at most the max of each component. Restates the archimedean property of the p-adic norm.

source
theorem padic_norm.add_eq_max_of_ne (p : ℕ) [hp : fact (nat.prime p)] {q r : ℚ} (hne : padic_norm p q ≠ padic_norm p r) :
padic_norm p (q + r) = max (padic_norm p q) (padic_norm p r)

If the p-adic norms of q and r are different, then the norm of q + r is equal to the max of the norms of q and r.

source
@[protected, instance]
def padic_norm.is_absolute_value (p : ℕ) [hp : fact (nat.prime p)] :
is_absolute_value (padic_norm p)

The p-adic norm is an absolute value: positive-definite and multiplicative, satisfying the triangle inequality.

source
theorem padic_norm.dvd_iff_norm_le {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {z : ℤ} :
↑(p ^ n) ∣ z ↔ padic_norm p ↑z ≤ ↑p ^ -↑n