mathlib3 documentation

number_theory.padics.padic_norm

p-adic norm #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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 p.prime] as a type class argument.

References #

Tags #

p-adic, p adic, padic, norm, valuation

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)

Instances for padic_norm

padic_norm.is_absolute_value

@[protected, simp]

theorem padic_norm.eq_zpow_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 = (↑p)⁻¹

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

See also padic_norm.padic_norm_p_of_prime for a version assuming p is prime.

@[simp]

theorem padic_norm.padic_norm_p_of_prime {p : ℕ} [fact (nat.prime p)] :

padic_norm p ↑p = (↑p)⁻¹

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

See also padic_norm.padic_norm_p for a version assuming 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 p is prime.

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) ≤ linear_order.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) ≤ linear_order.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) = linear_order.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

theorem padic_norm.int_eq_one_iff {p : ℕ} [hp : fact (nat.prime p)] (m : ℤ) :

padic_norm p ↑m = 1 ↔ ¬↑p ∣ m

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

theorem padic_norm.int_lt_one_iff {p : ℕ} [hp : fact (nat.prime p)] (m : ℤ) :

padic_norm p ↑m < 1 ↔ ↑p ∣ m

theorem padic_norm.of_nat {p : ℕ} [hp : fact (nat.prime p)] (m : ℕ) :

padic_norm p ↑m ≤ 1

theorem padic_norm.nat_eq_one_iff {p : ℕ} [hp : fact (nat.prime p)] (m : ℕ) :

padic_norm p ↑m = 1 ↔ ¬p ∣ m

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

theorem padic_norm.nat_lt_one_iff {p : ℕ} [hp : fact (nat.prime p)] (m : ℕ) :

padic_norm p ↑m < 1 ↔ p ∣ m

theorem padic_norm.sum_lt {p : ℕ} [hp : fact (nat.prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : finset α} :

s.nonempty → (∀ (i : α), i ∈ s → padic_norm p (F i) < t) → padic_norm p (s.sum (λ (i : α), F i)) < t

theorem padic_norm.sum_le {p : ℕ} [hp : fact (nat.prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : finset α} :

s.nonempty → (∀ (i : α), i ∈ s → padic_norm p (F i) ≤ t) → padic_norm p (s.sum (λ (i : α), F i)) ≤ t

theorem padic_norm.sum_lt' {p : ℕ} [hp : fact (nat.prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : finset α} (hF : ∀ (i : α), i ∈ s → padic_norm p (F i) < t) (ht : 0 < t) :

padic_norm p (s.sum (λ (i : α), F i)) < t

theorem padic_norm.sum_le' {p : ℕ} [hp : fact (nat.prime p)] {α : Type u_1} {F : α → ℚ} {t : ℚ} {s : finset α} (hF : ∀ (i : α), i ∈ s → padic_norm p (F i) ≤ t) (ht : 0 ≤ t) :

padic_norm p (s.sum (λ (i : α), F i)) ≤ t