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  :

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
theorem padic_val_rat_def (p : ) [hp : fact (nat.prime p)] {q : } (hq : q 0) :

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

@[simp]
theorem padic_val_rat.neg {p : } (q : ) :

padic_val_rat p q is symmetric in q.

@[simp]
theorem padic_val_rat.one {p : } :

padic_val_rat p 1 is 0 for any p.

@[simp]
theorem padic_val_rat.padic_val_rat_self {p : } :
1 < ppadic_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) :

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

def padic_val_nat  :

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

Equations

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

@[simp]

padic_val_rat coincides with padic_val_nat.

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

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)] :
n 0p n1 padic_val_nat p n

@[simp]
theorem padic_val_nat_zero (m : ) :

@[simp]
theorem padic_val_nat_one (m : ) :

theorem padic_val_rat.finite_int_prime_iff {p : } [p_prime : fact (nat.prime p)] {a : } :

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

theorem padic_val_rat.defn (p : ) [p_prime : fact (nat.prime p)] {q : } {n d : } (hqz : q 0) (qdf : q = n /. d) :

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

theorem padic_val_rat.mul (p : ) [p_prime : fact (nat.prime p)] {q r : } :
q 0r 0padic_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.pow (p : ) [p_prime : fact (nat.prime p)] {q : } (hq : q 0) {k : } :

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

theorem padic_val_rat.inv (p : ) [p_prime : fact (nat.prime p)] {q : } :

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

theorem padic_val_rat.div (p : ) [p_prime : fact (nat.prime p)] {q r : } :
q 0r 0padic_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₂ : } :
n₁ 0n₂ 0d₁ 0d₂ 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 : } :
q 0r 0q + r 0padic_val_rat p q padic_val_rat p rpadic_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 : } :
q 0r 0q + r 0min (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_nat.mul (p : ) [p_prime : fact (nat.prime p)] {q r : } :
q 0r 0padic_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.

theorem padic_val_nat.div {p : } [p_prime : fact (nat.prime p)] {b : } :
p bpadic_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 : } :
¬p npadic_val_nat p n = 0

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

theorem padic_val_nat_primes {p q : } [p_prime : fact (nat.prime p)] [q_prime : fact (nat.prime q)] :
p qpadic_val_nat p q = 0

theorem padic_val_nat.div' {p : } [p_prime : fact (nat.prime p)] {m : } (cpm : p.coprime m) {b : } :
m bpadic_val_nat p (b / m) = padic_val_nat p b

theorem prod_pow_prime_padic_val_nat (n : ) (hn : n 0) (m : ) :
n < m∏ (p : ) in finset.filter nat.prime (finset.range m), p ^ padic_val_nat p n = n

def padic_norm  :

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
@[simp]
theorem padic_norm.eq_fpow_of_nonzero (p : ) {q : } :
q 0padic_norm p q = p ^ -padic_val_rat p q

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

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

The p-adic norm is nonnegative.

@[simp]
theorem padic_norm.zero (p : ) :

The p-adic norm of 0 is 0.

@[simp]
theorem padic_norm.one (p : ) :

The p-adic norm of 1 is 1.

theorem padic_norm.padic_norm_p {p : } :
1 < ppadic_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]

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_p_lt_one {p : } :
1 < ppadic_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.

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.

theorem padic_norm.values_discrete (p : ) {q : } :
q 0(∃ (z : ), padic_norm p q = p ^ -z)

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

@[simp]
theorem padic_norm.neg (p : ) (q : ) :

padic_norm p is symmetric.

theorem padic_norm.nonzero (p : ) [hp : fact (nat.prime p)] {q : } :
q 0padic_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 : } :
padic_norm p q = 0q = 0

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

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

@[simp]
theorem padic_norm.div (p : ) [hp : fact (nat.prime p)] (q r : ) :

The p-adic norm respects division.

theorem padic_norm.of_int (p : ) [hp : fact (nat.prime p)] (z : ) :

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

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

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.

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 : } :
padic_norm p q padic_norm p rpadic_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.

@[instance]

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 : } :