A small p-adic valuation toolkit on ℚ and ℚ[X]

• VG p q r : q = 0 ∨ r ≤ v_p(q) (with a rational lower bound r);
• GV p f r : every coefficient of f ∈ ℚ[X] satisfies VG p · r (Gauss valuation bound);
• det_GV : if M i j has Gauss valuation ≥ ρ i + κ j, then det M has ≥ ∑ ρ + ∑ κ.

def Zeta5Irrational.VG (p : ℕ) (q r : ℚ) : Prop

v_p(q) ≥ r (vacuous for q = 0).

Equations

• Zeta5Irrational.VG p q r = (q = 0 ∨ r ≤ ↑(padicValRat p q))

theorem Zeta5Irrational.VG.zero {p : ℕ} (r : ℚ) : VG p 0 r

theorem Zeta5Irrational.VG.mono {p : ℕ} {q r s : ℚ} (h : VG p q r) (hs : s ≤ r) : VG p q s

theorem Zeta5Irrational.VG.neg {p : ℕ} {q r : ℚ} (h : VG p q r) : VG p (-q) r

theorem Zeta5Irrational.VG.add {p : ℕ} [Fact (Nat.Prime p)] {q q' r : ℚ} (h : VG p q r) (h' : VG p q' r) : VG p (q + q') r

theorem Zeta5Irrational.VG.sub {p : ℕ} [Fact (Nat.Prime p)] {q q' r : ℚ} (h : VG p q r) (h' : VG p q' r) : VG p (q - q') r

theorem Zeta5Irrational.VG.mul {p : ℕ} [Fact (Nat.Prime p)] {q q' r r' : ℚ} (h : VG p q r) (h' : VG p q' r') : VG p (q * q') (r + r')

theorem Zeta5Irrational.VG.sum {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {f : ι → ℚ} {r : ℚ} (h : ∀ i ∈ s, VG p (f i) r) : VG p (∑ i ∈ s, f i) r

theorem Zeta5Irrational.VG.prod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {f r : ι → ℚ} (h : ∀ i ∈ s, VG p (f i) (r i)) : VG p (∏ i ∈ s, f i) (∑ i ∈ s, r i)

theorem Zeta5Irrational.VG.intCast {p : ℕ} (z : ℤ) : VG p (↑z) 0

theorem Zeta5Irrational.VG.natCast {p : ℕ} (n : ℕ) : VG p (↑n) 0

theorem Zeta5Irrational.VG.one {p : ℕ} : VG p 1 0

theorem Zeta5Irrational.VG.inv {p : ℕ} [Fact (Nat.Prime p)] {q r : ℚ} (_h : q ≠ 0) (hv : ↑(padicValRat p q) ≤ r) : VG p q⁻¹ (-r)

theorem Zeta5Irrational.VG.of_eq {p : ℕ} {q : ℚ} (r : ℚ) (h : q ≠ 0 → r ≤ ↑(padicValRat p q)) : VG p q r

theorem Zeta5Irrational.VG.primePow {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℤ) : VG p (↑p ^ k) ↑k

v_p(p^k) = k.

theorem Zeta5Irrational.VG.zpow_mul {p : ℕ} [Fact (Nat.Prime p)] {q r : ℚ} (k : ℤ) (h : VG p q r) : VG p (↑p ^ k * q) (↑k + r)

theorem Zeta5Irrational.VG.pow {p : ℕ} [Fact (Nat.Prime p)] {q r : ℚ} (h : VG p q r) (n : ℕ) : VG p (q ^ n) (↑n * r)

theorem Zeta5Irrational.VG.inv_nat {p : ℕ} [hp : Fact (Nat.Prime p)] {j n : ℕ} (hj : 1 ≤ j) (hjn : j ≤ n) : VG p (↑j)⁻¹ (-↑(Nat.log p n))

A lower bound on the valuation of 1 / j for 1 ≤ j ≤ n.

def Zeta5Irrational.GV (p : ℕ) (f : Polynomial ℚ) (r : ℚ) : Prop

Gauss valuation bound for polynomials in X.

Equations

• Zeta5Irrational.GV p f r = ∀ (n : ℕ), Zeta5Irrational.VG p (f.coeff n) r

theorem Zeta5Irrational.GV.zero {p : ℕ} (r : ℚ) : GV p 0 r

theorem Zeta5Irrational.GV.mono {p : ℕ} {f : Polynomial ℚ} {r s : ℚ} (h : GV p f r) (hs : s ≤ r) : GV p f s

theorem Zeta5Irrational.GV.add {p : ℕ} [Fact (Nat.Prime p)] {f g : Polynomial ℚ} {r : ℚ} (hf : GV p f r) (hg : GV p g r) : GV p (f + g) r

theorem Zeta5Irrational.GV.neg {p : ℕ} {f : Polynomial ℚ} {r : ℚ} (hf : GV p f r) : GV p (-f) r

theorem Zeta5Irrational.GV.sub {p : ℕ} [Fact (Nat.Prime p)] {f g : Polynomial ℚ} {r : ℚ} (hf : GV p f r) (hg : GV p g r) : GV p (f - g) r

theorem Zeta5Irrational.GV.C {p : ℕ} {q r : ℚ} (h : VG p q r) : GV p (Polynomial.C q) r

theorem Zeta5Irrational.GV.X {p : ℕ} : GV p Polynomial.X 0

theorem Zeta5Irrational.GV.mul {p : ℕ} [Fact (Nat.Prime p)] {f g : Polynomial ℚ} {r s : ℚ} (hf : GV p f r) (hg : GV p g s) : GV p (f * g) (r + s)

theorem Zeta5Irrational.GV.C_mul {p : ℕ} [Fact (Nat.Prime p)] {q r s : ℚ} {f : Polynomial ℚ} (hq : VG p q r) (hf : GV p f s) : GV p (Polynomial.C q * f) (r + s)

theorem Zeta5Irrational.GV.sum {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {f : ι → Polynomial ℚ} {r : ℚ} (h : ∀ i ∈ s, GV p (f i) r) : GV p (∑ i ∈ s, f i) r

theorem Zeta5Irrational.GV.prod {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) {f : ι → Polynomial ℚ} {r : ι → ℚ} (h : ∀ i ∈ s, GV p (f i) (r i)) : GV p (∏ i ∈ s, f i) (∑ i ∈ s, r i)

theorem Zeta5Irrational.det_GV {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι (Polynomial ℚ)) (ρ κ : ι → ℚ) (h : ∀ (i j : ι), GV p (M i j) (ρ i + κ j)) : GV p M.det (∑ i : ι, ρ i + ∑ j : ι, κ j)

Determinant bound with row and column weights.