Documentation

Mathlib.NumberTheory.Padics.PadicNorm

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]

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.

Equations

padicNorm p q = if q = 0 then 0 else ↑p ^ (-padicValRat p q)

Instances For

@[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)] (neq : 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.instIsAbsoluteValueRatInstOrderedSemiringRatSemiringPadicNorm {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.

Equations

(_ : IsAbsoluteValue (padicNorm p)) = (_ : IsAbsoluteValue (padicNorm p))

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

¬Rat.isInt a = 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 (Finset.sum s fun (i : α) => 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 (Finset.sum s fun (i : α) => 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 (Finset.sum s fun (i : α) => 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 (Finset.sum s fun (i : α) => F i) ≤ t