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
- [F. Q. Gouêva, 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
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.
A simplification of the definition of padic_val_rat p q when q ≠ 0 and p is prime.
padic_val_rat p q is symmetric in q.
padic_val_rat p 1 is 0 for any p.
For p ≠ 0, p ≠ 1,padic_val_rat p p` is 1.
The p-adic value of an integer z ≠ 0 is the multiplicity of p in z.
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
padic_val_nat is defined as an int.to_nat cast; this lemma ensures that the cast is well-behaved.
padic_val_rat coincides with padic_val_nat.
A simplification of padic_val_nat when one input is prime, by analogy with padic_val_rat_def.
The multiplicity of p : ℕ in a : ℤ is finite exactly when a ≠ 0.
A rewrite lemma for padic_val_rat p q when q is expressed in terms of rat.mk.
A rewrite lemma for padic_val_rat p (q * r) with conditions q ≠ 0, r ≠ 0.
A rewrite lemma for padic_val_rat p (q^k) with conditionq ≠ 0`.
A rewrite lemma for padic_val_rat p (q⁻¹) with condition q ≠ 0.
A rewrite lemma for padic_val_rat p (q / r) with conditions q ≠ 0, r ≠ 0.
A condition for padic_val_rat p (n₁ / d₁) ≤ padic_val_rat p (n₂ / d₂),
in terms of divisibility byp^n`.
Sufficient conditions to show that the p-adic valuation of q is less than or equal to the
p-adic vlauation of q + r.
The minimum of the valuations of q and r is less than or equal to the valuation of q + r.
A rewrite lemma for padic_val_nat p (q * r) with conditions q ≠ 0, r ≠ 0.
Dividing out by a prime factor reduces the padic_val_nat by 1.
If a prime doesn't appear in n, padic_val_nat p n is 0.
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)
Unfolds the definition of the p-adic norm of q when q ≠ 0.
The p-adic norm is nonnegative.
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.
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.
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.
padic_norm p q takes discrete values p ^ -z for z : ℤ.
If q ≠ 0, then padic_norm p q ≠ 0.
padic_norm p is symmetric.
If the p-adic norm of q is 0, then q is 0.
The p-adic norm is multiplicative.
The p-adic norm respects division.
The p-adic norm of an integer is at most 1.
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.
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.
The p-adic norm of a difference is at most the max of each component. Restates the archimedean property of the p-adic norm.
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.
The p-adic norm is an absolute value: positive-definite and multiplicative, satisfying the triangle inequality.
Equations
- _ = _