Documentation

Mathlib.NumberTheory.Padics.PadicVal

p-adic Valuation #

This file defines the p-adic valuation on , , and .

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 p-adic valuations on and agree with that on .

The valuation induces a norm on . This norm is defined in padicNorm.lean.

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.

Calculations with p-adic valuations #

References #

Tags #

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

def padicValNat (p : ) (n : ) :

For p ≠ 1, the p-adic valuation of a natural n ≠ 0 is the largest natural number k such that p^k divides n. If n = 0 or p = 1, then padicValNat p q defaults to 0.

Equations
Instances For
    @[simp]
    theorem padicValNat.zero {p : } :

    padicValNat p 0 is 0 for any p.

    @[simp]
    theorem padicValNat.one {p : } :

    padicValNat p 1 is 0 for any p.

    @[simp]
    theorem padicValNat.self {p : } (hp : 1 < p) :

    If p ≠ 0 and p ≠ 1, then padicValNat p p is 1.

    @[simp]
    theorem padicValNat.eq_zero_iff {p : } {n : } :
    padicValNat p n = 0 p = 1 n = 0 ¬p n
    theorem padicValNat.eq_zero_of_not_dvd {p : } {n : } (h : ¬p n) :
    theorem padicValNat.maxPowDiv_eq_multiplicity {p : } {n : } (hp : 1 < p) (hn : 0 < n) :
    (p.maxPowDiv n) = multiplicity p n
    theorem padicValNat.maxPowDiv_eq_multiplicity_get {p : } {n : } (hp : 1 < p) (hn : 0 < n) (h : multiplicity.Finite p n) :
    p.maxPowDiv n = (multiplicity p n).get h
    @[csimp]

    Allows for more efficient code for padicValNat

    def padicValInt (p : ) (z : ) :

    For p ≠ 1, the p-adic valuation of an integer z ≠ 0 is the largest natural number k such that p^k divides z. If x = 0 or p = 1, then padicValInt p q defaults to 0.

    Equations
    Instances For
      theorem padicValInt.of_ne_one_ne_zero {p : } {z : } (hp : p 1) (hz : z 0) :
      padicValInt p z = (multiplicity (p) z).get
      @[simp]
      theorem padicValInt.zero {p : } :

      padicValInt p 0 is 0 for any p.

      @[simp]
      theorem padicValInt.one {p : } :

      padicValInt p 1 is 0 for any p.

      @[simp]
      theorem padicValInt.of_nat {p : } {n : } :

      The p-adic value of a natural is its p-adic value as an integer.

      theorem padicValInt.self {p : } (hp : 1 < p) :
      padicValInt p p = 1

      If p ≠ 0 and p ≠ 1, then padicValInt p p is 1.

      theorem padicValInt.eq_zero_of_not_dvd {p : } {z : } (h : ¬p z) :
      def padicValRat (p : ) (q : ) :

      padicValRat defines the valuation of a rational q to be the valuation of q.num minus the valuation of q.den. If q = 0 or p = 1, then padicValRat p q defaults to 0.

      Equations
      Instances For
        theorem padicValRat_def (p : ) (q : ) :
        padicValRat p q = (padicValInt p q.num) - (padicValNat p q.den)
        @[simp]
        theorem padicValRat.neg {p : } (q : ) :

        padicValRat p q is symmetric in q.

        @[simp]
        theorem padicValRat.zero {p : } :

        padicValRat p 0 is 0 for any p.

        @[simp]
        theorem padicValRat.one {p : } :

        padicValRat p 1 is 0 for any p.

        @[simp]
        theorem padicValRat.of_int {p : } {z : } :
        padicValRat p z = (padicValInt p z)

        The p-adic value of an integer z ≠ 0 is its p-adic_value as a rational.

        theorem padicValRat.of_int_multiplicity {p : } {z : } (hp : p 1) (hz : z 0) :
        padicValRat p z = ((multiplicity (p) z).get )

        The p-adic value of an integer z ≠ 0 is the multiplicity of p in z.

        theorem padicValRat.multiplicity_sub_multiplicity {p : } {q : } (hp : p 1) (hq : q 0) :
        padicValRat p q = ((multiplicity (p) q.num).get ) - ((multiplicity p q.den).get )
        @[simp]
        theorem padicValRat.of_nat {p : } {n : } :
        padicValRat p n = (padicValNat p n)

        The p-adic value of an integer z ≠ 0 is its p-adic value as a rational.

        theorem padicValRat.self {p : } (hp : 1 < p) :
        padicValRat p p = 1

        If p ≠ 0 and p ≠ 1, then padicValRat p p is 1.

        theorem padicValRat_of_nat {p : } (n : ) :
        (padicValNat p n) = padicValRat p n

        padicValRat coincides with padicValNat.

        theorem padicValNat_def {p : } [hp : Fact (Nat.Prime p)] {n : } (hn : 0 < n) :
        padicValNat p n = (multiplicity p n).get

        A simplification of padicValNat when one input is prime, by analogy with padicValRat_def.

        theorem padicValNat_def' {p : } {n : } (hp : p 1) (hn : 0 < n) :
        @[simp]
        theorem padicValNat_self {p : } [Fact (Nat.Prime p)] :
        theorem one_le_padicValNat_of_dvd {p : } {n : } [hp : Fact (Nat.Prime p)] (hn : 0 < n) (div : p n) :
        theorem dvd_iff_padicValNat_ne_zero {p : } {n : } [Fact (Nat.Prime p)] (hn0 : n 0) :
        theorem le_multiplicity_iff_replicate_subperm_factors {a : } {b : } {n : } (ha : Nat.Prime a) (hb : b 0) :
        n multiplicity a b (List.replicate n a).Subperm b.factors
        theorem le_padicValNat_iff_replicate_subperm_factors {a : } {b : } {n : } (ha : Nat.Prime a) (hb : b 0) :
        n padicValNat a b (List.replicate n a).Subperm b.factors
        theorem padicValRat.finite_int_prime_iff {p : } [hp : Fact (Nat.Prime p)] {a : } :

        The multiplicity of p : ℕ in a : ℤ is finite exactly when a ≠ 0.

        theorem padicValRat.defn (p : ) [hp : Fact (Nat.Prime p)] {q : } {n : } {d : } (hqz : q 0) (qdf : q = Rat.divInt n d) :
        padicValRat p q = ((multiplicity (p) n).get ) - ((multiplicity (p) d).get )

        A rewrite lemma for padicValRat p q when q is expressed in terms of Rat.mk.

        theorem padicValRat.mul {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hq : q 0) (hr : r 0) :

        A rewrite lemma for padicValRat p (q * r) with conditions q ≠ 0, r ≠ 0.

        theorem padicValRat.pow {p : } [hp : Fact (Nat.Prime p)] {q : } (hq : q 0) {k : } :
        padicValRat p (q ^ k) = k * padicValRat p q

        A rewrite lemma for padicValRat p (q^k) with condition q ≠ 0.

        theorem padicValRat.inv {p : } [hp : Fact (Nat.Prime p)] (q : ) :

        A rewrite lemma for padicValRat p (q⁻¹) with condition q ≠ 0.

        theorem padicValRat.div {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hq : q 0) (hr : r 0) :

        A rewrite lemma for padicValRat p (q / r) with conditions q ≠ 0, r ≠ 0.

        theorem padicValRat.padicValRat_le_padicValRat_iff {p : } [hp : Fact (Nat.Prime p)] {n₁ : } {n₂ : } {d₁ : } {d₂ : } (hn₁ : n₁ 0) (hn₂ : n₂ 0) (hd₁ : d₁ 0) (hd₂ : d₂ 0) :
        padicValRat p (Rat.divInt n₁ d₁) padicValRat p (Rat.divInt n₂ d₂) ∀ (n : ), p ^ n n₁ * d₂p ^ n n₂ * d₁

        A condition for padicValRat p (n₁ / d₁) ≤ padicValRat p (n₂ / d₂), in terms of divisibility by p^n.

        theorem padicValRat.le_padicValRat_add_of_le {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) (h : padicValRat p q padicValRat p r) :

        Sufficient conditions to show that the p-adic valuation of q is less than or equal to the p-adic valuation of q + r.

        theorem padicValRat.min_le_padicValRat_add {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) :

        The minimum of the valuations of q and r is at most the valuation of q + r.

        theorem padicValRat.add_eq_min {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) (hq : q 0) (hr : r 0) (hval : padicValRat p q padicValRat p r) :

        Ultrametric property of a p-adic valuation.

        theorem padicValRat.add_eq_of_lt {p : } [hp : Fact (Nat.Prime p)] {q : } {r : } (hqr : q + r 0) (hq : q 0) (hr : r 0) (hval : padicValRat p q < padicValRat p r) :
        theorem padicValRat.lt_add_of_lt {p : } [hp : Fact (Nat.Prime p)] {q : } {r₁ : } {r₂ : } (hqr : r₁ + r₂ 0) (hval₁ : padicValRat p q < padicValRat p r₁) (hval₂ : padicValRat p q < padicValRat p r₂) :
        padicValRat p q < padicValRat p (r₁ + r₂)
        @[simp]
        theorem padicValRat.self_pow_inv {p : } [hp : Fact (Nat.Prime p)] (r : ) :
        padicValRat p (p ^ r)⁻¹ = -r
        theorem padicValRat.sum_pos_of_pos {p : } [hp : Fact (Nat.Prime p)] {n : } {F : } (hF : i < n, 0 < padicValRat p (F i)) (hn0 : iFinset.range n, F i 0) :
        0 < padicValRat p (iFinset.range n, F i)

        A finite sum of rationals with positive p-adic valuation has positive p-adic valuation (if the sum is non-zero).

        theorem padicValRat.lt_sum_of_lt {p : } {j : } [hp : Fact (Nat.Prime p)] {F : } {S : Finset } (hS : S.Nonempty) (hF : iS, padicValRat p (F j) < padicValRat p (F i)) (hn1 : ∀ (i : ), 0 < F i) :
        padicValRat p (F j) < padicValRat p (iS, F i)

        If the p-adic valuation of a finite set of positive rationals is greater than a given rational number, then the p-adic valuation of their sum is also greater than the same rational number.

        theorem padicValNat.mul {p : } {a : } {b : } [hp : Fact (Nat.Prime p)] :
        a 0b 0padicValNat p (a * b) = padicValNat p a + padicValNat p b

        A rewrite lemma for padicValNat p (a * b) with conditions a ≠ 0, b ≠ 0.

        theorem padicValNat.div_of_dvd {p : } {a : } {b : } [hp : Fact (Nat.Prime p)] (h : b a) :
        theorem padicValNat.div {p : } {b : } [hp : Fact (Nat.Prime p)] (dvd : p b) :
        padicValNat p (b / p) = padicValNat p b - 1

        Dividing out by a prime factor reduces the padicValNat by 1.

        theorem padicValNat.pow {p : } {a : } [hp : Fact (Nat.Prime p)] (n : ) (ha : a 0) :
        padicValNat p (a ^ n) = n * padicValNat p a

        A version of padicValRat.pow for padicValNat.

        @[simp]
        theorem padicValNat.prime_pow {p : } [hp : Fact (Nat.Prime p)] (n : ) :
        padicValNat p (p ^ n) = n
        theorem padicValNat.div_pow {p : } {a : } {b : } [hp : Fact (Nat.Prime p)] (dvd : p ^ a b) :
        padicValNat p (b / p ^ a) = padicValNat p b - a
        theorem padicValNat.div' {p : } [hp : Fact (Nat.Prime p)] {m : } (cpm : p.Coprime m) {b : } (dvd : m b) :
        theorem dvd_of_one_le_padicValNat {p : } {n : } (hp : 1 padicValNat p n) :
        p n
        theorem pow_padicValNat_dvd {p : } {n : } :
        p ^ padicValNat p n n
        theorem padicValNat_dvd_iff_le {p : } [hp : Fact (Nat.Prime p)] {a : } {n : } (ha : a 0) :
        p ^ n a n padicValNat p a
        theorem padicValNat_dvd_iff {p : } (n : ) [hp : Fact (Nat.Prime p)] (a : ) :
        p ^ n a a = 0 n padicValNat p a
        theorem pow_succ_padicValNat_not_dvd {p : } {n : } [hp : Fact (Nat.Prime p)] (hn : n 0) :
        ¬p ^ (padicValNat p n + 1) n
        theorem padicValNat_primes {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (neq : p q) :
        theorem padicValNat_prime_prime_pow {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ) (neq : p q) :
        padicValNat p (q ^ n) = 0
        theorem padicValNat_mul_pow_left {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ) (m : ) (neq : p q) :
        padicValNat p (p ^ n * q ^ m) = n
        theorem padicValNat_mul_pow_right {p : } {q : } [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (n : ) (m : ) (neq : q p) :
        padicValNat q (p ^ n * q ^ m) = m
        theorem padicValNat_le_nat_log {p : } (n : ) :

        The p-adic valuation of n is less than or equal to its logarithm w.r.t p.

        theorem nat_log_eq_padicValNat_iff {p : } {n : } [hp : Fact (Nat.Prime p)] (hn : 0 < n) :
        Nat.log p n = padicValNat p n n < p ^ (padicValNat p n + 1)

        The p-adic valuation of n is equal to the logarithm w.r.t p iff n is less than p raised to one plus the p-adic valuation of n.

        theorem Nat.log_ne_padicValNat_succ {n : } (hn : n 0) :
        Nat.log 2 n padicValNat 2 (n + 1)
        theorem range_pow_padicValNat_subset_divisors {p : } {n : } (hn : n 0) :
        Finset.image (fun (x : ) => p ^ x) (Finset.range (padicValNat p n + 1)) n.divisors
        theorem range_pow_padicValNat_subset_divisors' {p : } {n : } [hp : Fact (Nat.Prime p)] :
        Finset.image (fun (t : ) => p ^ (t + 1)) (Finset.range (padicValNat p n)) n.divisors.erase 1
        theorem padicValNat_factorial_mul {p : } (n : ) [hp : Fact (Nat.Prime p)] :
        padicValNat p (p * n).factorial = padicValNat p n.factorial + n

        The p-adic valuation of (p * n)! is n more than that of n!.

        theorem padicValNat_eq_zero_of_mem_Ioo {p : } {m : } {k : } (hm : m Set.Ioo (p * k) (p * (k + 1))) :

        The p-adic valuation of m equals zero if it is between p * k and p * (k + 1) for some k.

        theorem padicValNat_factorial_mul_add {p : } {n : } (m : ) [hp : Fact (Nat.Prime p)] (h : n < p) :
        padicValNat p (p * m + n).factorial = padicValNat p (p * m).factorial
        @[simp]
        theorem padicValNat_mul_div_factorial {p : } (n : ) [hp : Fact (Nat.Prime p)] :
        padicValNat p (p * (n / p)).factorial = padicValNat p n.factorial

        The p-adic valuation of n! is equal to the p-adic valuation of the factorial of the largest multiple of p below n, i.e. (p * ⌊n / p⌋)!.

        theorem padicValNat_factorial {p : } {n : } {b : } [hp : Fact (Nat.Prime p)] (hnb : Nat.log p n < b) :
        padicValNat p n.factorial = iFinset.Ico 1 b, n / p ^ i

        Legendre's Theorem

        The p-adic valuation of n! is the sum of the quotients n / p ^ i. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

        theorem sub_one_mul_padicValNat_factorial {p : } [hp : Fact (Nat.Prime p)] (n : ) :
        (p - 1) * padicValNat p n.factorial = n - (p.digits n).sum

        Legendre's Theorem

        Taking (p - 1) times the p-adic valuation of n! equals n minus the sum of base p digits of n.

        theorem padicValNat_choose {p : } {n : } {k : } {b : } [hp : Fact (Nat.Prime p)] (hkn : k n) (hnb : Nat.log p n < b) :
        padicValNat p (n.choose k) = (Finset.filter (fun (i : ) => p ^ i k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card

        Kummer's Theorem

        The p-adic valuation of n.choose k is the number of carries when k and n - k are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p n.

        theorem padicValNat_choose' {p : } {n : } {k : } {b : } [hp : Fact (Nat.Prime p)] (hnb : Nat.log p (n + k) < b) :
        padicValNat p ((n + k).choose k) = (Finset.filter (fun (i : ) => p ^ i k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card

        Kummer's Theorem

        The p-adic valuation of (n + k).choose k is the number of carries when k and n are added in base p. This sum is expressed over the finset Ico 1 b where b is any bound greater than log p (n + k).

        theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits' {p : } {k : } {n : } [hp : Fact (Nat.Prime p)] :
        (p - 1) * padicValNat p ((n + k).choose k) = (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

        Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n + k over k equals the sum of the digits of k plus the sum of the digits of n minus the sum of digits of n + k, all base p.

        theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {p : } {k : } {n : } [hp : Fact (Nat.Prime p)] (h : k n) :
        (p - 1) * padicValNat p (n.choose k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum

        Kummer's Theorem Taking (p - 1) times the p-adic valuation of the binomial n over k equals the sum of the digits of k plus the sum of the digits of n - k minus the sum of digits of n, all base p.

        theorem padicValInt_dvd_iff {p : } [hp : Fact (Nat.Prime p)] (n : ) (a : ) :
        p ^ n a a = 0 n padicValInt p a
        theorem padicValInt_dvd {p : } [hp : Fact (Nat.Prime p)] (a : ) :
        p ^ padicValInt p a a
        theorem padicValInt_self {p : } [hp : Fact (Nat.Prime p)] :
        padicValInt p p = 1
        theorem padicValInt.mul {p : } [hp : Fact (Nat.Prime p)] {a : } {b : } (ha : a 0) (hb : b 0) :
        theorem padicValInt_mul_eq_succ {p : } [hp : Fact (Nat.Prime p)] (a : ) (ha : a 0) :
        padicValInt p (a * p) = padicValInt p a + 1