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 #

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

    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]

    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.

    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 is symmetric.

    theorem padicNorm.nonzero {p : } [hp : Fact (Nat.Prime p)] {q : } (hq : 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 : ) :

    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.

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

    Equations
    • =
    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) :

    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(is, 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(is, 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 : is, 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 : is, padicNorm p (F i) t) (ht : 0 t) :
    padicNorm p (Finset.sum s fun (i : α) => F i) t