p-adic norm

This file defines 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 ∈ ℤ}.

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.

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 padicNorm (p : ℕ) (q : ℚ) : ℚ

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

@[simp]

theorem padicNorm.eq_zpow_of_nonzero {p : ℕ} {q : ℚ} (hq : q ≠ 0) : padicNorm p q = ↑p ^ (-padicValRat p q)

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

theorem padicNorm.nonneg {p : ℕ} (q : ℚ) : 0 ≤ padicNorm p q

The p-adic norm is nonnegative.

@[simp]

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

The p-adic norm of 0 is 0.

theorem padicNorm.one {p : ℕ} : padicNorm p 1 = 1

The p-adic norm of 1 is 1.

theorem padicNorm.padicNorm_p {p : ℕ} (hp : 1 < p) : padicNorm p ↑p = (↑p)⁻¹

The p-adic norm of p is p⁻¹ if p > 1.

See also padicNorm.padicNorm_p_of_prime for a version assuming p is prime.

@[simp]

theorem padicNorm.padicNorm_p_of_prime {p : ℕ} [Fact (Nat.Prime p)] : padicNorm p ↑p = (↑p)⁻¹

The p-adic norm of p is p⁻¹ if p is prime.

See also padicNorm.padicNorm_p for a version assuming 1 < p.

theorem padicNorm.padicNorm_of_prime_of_ne {p q : ℕ} [p_prime : Fact (Nat.Prime p)] [q_prime : Fact (Nat.Prime q)] (ne : p ≠ q) : padicNorm p ↑q = 1

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

theorem padicNorm.padicNorm_p_lt_one {p : ℕ} (hp : 1 < p) : padicNorm p ↑p < 1

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

See also padicNorm.padicNorm_p_lt_one_of_prime for a version assuming p is prime.

theorem padicNorm.padicNorm_p_lt_one_of_prime {p : ℕ} [Fact (Nat.Prime p)] : padicNorm p ↑p < 1

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

See also padicNorm.padicNorm_p_lt_one for a version assuming 1 < p.

theorem padicNorm.values_discrete {p : ℕ} {q : ℚ} (hq : q ≠ 0) : ∃ (z : ℤ), padicNorm p q = ↑p ^ (-z)

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

@[simp]

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

padicNorm p is symmetric.

theorem padicNorm.nonzero {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} (hq : q ≠ 0) : padicNorm p q ≠ 0

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

theorem padicNorm.zero_of_padicNorm_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {q : ℚ} (h : padicNorm p q = 0) : q = 0

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

@[simp]

theorem padicNorm.mul {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ) : padicNorm p (q * r) = padicNorm p q * padicNorm p r

The p-adic norm is multiplicative.

@[simp]

theorem padicNorm.div {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ) : padicNorm p (q / r) = padicNorm p q / padicNorm p r

The p-adic norm respects division.

theorem padicNorm.of_int {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ) : padicNorm p ↑z ≤ 1

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

theorem padicNorm.nonarchimedean {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} : padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm 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 padicNorm.triangle_ineq {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ) : padicNorm p (q + r) ≤ padicNorm p q + padicNorm 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.

theorem padicNorm.sub {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} : padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm 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 padicNorm.add_eq_max_of_ne {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ} (hne : padicNorm p q ≠ padicNorm p r) : padicNorm p (q + r) = max (padicNorm p q) (padicNorm 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 padicNorm.instIsAbsoluteValueRat {p : ℕ} [hp : Fact (Nat.Prime p)] : IsAbsoluteValue (padicNorm p)

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

theorem padicNorm.dvd_iff_norm_le {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)

theorem padicNorm.int_eq_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℤ) : padicNorm p ↑m = 1 ↔ ¬↑p ∣ m

The p-adic norm of an integer m is one iff p doesn't divide m.

theorem padicNorm.int_lt_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℤ) : padicNorm p ↑m < 1 ↔ ↑p ∣ m

theorem padicNorm.of_nat {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : padicNorm p ↑m ≤ 1

theorem padicNorm.nat_eq_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : padicNorm p ↑m = 1 ↔ ¬p ∣ m

The p-adic norm of a natural m is one iff p doesn't divide m.

theorem padicNorm.nat_lt_one_iff {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : padicNorm p ↑m < 1 ↔ p ∣ m

theorem padicNorm.not_int_of_not_padic_int (p : ℕ) {a : ℚ} [hp : Fact (Nat.Prime p)] (H : 1 < padicNorm p a) : ¬a.isInt = true

If a rational is not a p-adic integer, it is not an integer.

theorem padicNorm.sum_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α} : s.Nonempty → (∀ i ∈ s, padicNorm p (F i) < t) → padicNorm p (∑ i ∈ s, F i) < t

theorem padicNorm.sum_le {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α} : s.Nonempty → (∀ i ∈ s, padicNorm p (F i) ≤ t) → padicNorm p (∑ i ∈ s, F i) ≤ t

theorem padicNorm.sum_lt' {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α} (hF : ∀ i ∈ s, padicNorm p (F i) < t) (ht : 0 < t) : padicNorm p (∑ i ∈ s, F i) < t

theorem padicNorm.sum_le' {p : ℕ} [hp : Fact (Nat.Prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : Finset α} (hF : ∀ i ∈ s, padicNorm p (F i) ≤ t) (ht : 0 ≤ t) : padicNorm p (∑ i ∈ s, F i) ≤ t