mathlib documentation

data.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

def padic_val_rat (p : ℕ) (q : ℚ) :

For p ≠ 1, the p-adic valuation of an integer z ≠ 0 is the largest natural number n such that p^n divides z.

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

padic_val_rat p q = dite (q ≠ 0 ∧ p ≠ 1) (λ (h : q ≠ 0 ∧ p ≠ 1), ↑((multiplicity ↑p q.num).get _) - ↑((multiplicity ↑p ↑(q.denom)).get _)) (λ (h : ¬(q ≠ 0 ∧ p ≠ 1)), 0)

theorem padic_val_rat_def (p : ℕ) [hp : fact (nat.prime p)] {q : ℚ} (hq : q ≠ 0) :

padic_val_rat p q = ↑((multiplicity ↑p q.num).get _) - ↑((multiplicity ↑p ↑(q.denom)).get _)

A simplification of the definition of padic_val_rat p q when q ≠ 0 and p is prime.

@[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.

@[protected, simp]

theorem padic_val_rat.one {p : ℕ} :

padic_val_rat p 1 = 0

padic_val_rat p 1 is 0 for any p.

@[simp]

theorem padic_val_rat.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.

theorem padic_val_rat.padic_val_rat_of_int {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.

def padic_val_nat (p n : ℕ) :

A convenience function for the case of padic_val_rat when both inputs are natural numbers.

Equations

padic_val_nat p n = (padic_val_rat p ↑n).to_nat

theorem zero_le_padic_val_rat_of_nat (p n : ℕ) :

0 ≤ padic_val_rat p ↑n

padic_val_nat is defined as an int.to_nat cast; this lemma ensures that the cast is well-behaved.

@[simp, norm_cast]

theorem padic_val_rat_of_nat (p n : ℕ) :

↑(padic_val_nat p n) = padic_val_rat p ↑n

padic_val_rat coincides with padic_val_nat.

theorem padic_val_nat_def {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} (hn : n ≠ 0) :

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.

theorem one_le_padic_val_nat_of_dvd {n p : ℕ} [prime : fact (nat.prime p)] (nonzero : n ≠ 0) (div : p ∣ n) :

1 ≤ padic_val_nat p n

@[simp]

theorem padic_val_nat_zero (m : ℕ) :

padic_val_nat m 0 = 0

@[simp]

theorem padic_val_nat_one (m : ℕ) :

padic_val_nat m 1 = 0

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.

@[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.

@[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.

@[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 conditionq ≠ 0`.

@[protected]

theorem padic_val_rat.inv (p : ℕ) [p_prime : fact (nat.prime p)] {q : ℚ} (hq : q ≠ 0) :

padic_val_rat p q⁻¹ = -padic_val_rat p q

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

@[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.

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`.

theorem padic_val_rat.le_padic_val_rat_add_of_le (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) (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.

theorem padic_val_rat.min_le_padic_val_rat_add (p : ℕ) [p_prime : fact (nat.prime p)] {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) (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.

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).

@[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.

@[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.

theorem padic_val_nat_of_not_dvd {p : ℕ} [fact (nat.prime p)] {n : ℕ} (not_dvd : ¬p ∣ n) :

padic_val_nat p n = 0

If a prime doesn't appear in n, padic_val_nat p n is 0.

theorem dvd_of_one_le_padic_val_nat {n p : ℕ} [prime : fact (nat.prime p)] (hp : 1 ≤ padic_val_nat p n) :

p ∣ n

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

@[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

theorem padic_val_nat_eq_factors_count (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :

padic_val_nat p n = list.count p n.factors

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

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

padic_norm p q = ite (q = 0) 0 (↑p ^ -padic_val_rat p q)

@[protected, simp]

theorem padic_norm.eq_fpow_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.

@[protected]

theorem padic_norm.nonneg (p : ℕ) (q : ℚ) :

0 ≤ padic_norm p q

The p-adic norm is nonnegative.

@[protected, simp]

theorem padic_norm.zero (p : ℕ) :

padic_norm p 0 = 0

The p-adic norm of 0 is 0.

@[protected, simp]

theorem padic_norm.one (p : ℕ) :

padic_norm p 1 = 1

The p-adic norm of 1 is 1.

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.

@[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.

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.

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.

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.

@[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 : ℤ.

@[protected, simp]

theorem padic_norm.neg (p : ℕ) (q : ℚ) :

padic_norm p (-q) = padic_norm p q

padic_norm p is symmetric.

@[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.

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.

@[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.

@[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.

@[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.

@[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.

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.

@[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.

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.

@[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.

theorem padic_norm.dvd_iff_norm_le {p : ℕ} [hp : fact (nat.prime p)] {n : ℕ} {z : ℤ} :

↑(p ^ n) ∣ z ↔ padic_norm p ↑z ≤ ↑p ^ -↑n