The direct valuation bound for τ_X

For g = κ ∏_{ζ ∈ Z} (x - ζ) / ∏_{r ∈ Pl} (x - r) with p ≥ 5, poles in the same residue class differing by exactly one power of p, harmonic indices < p² and polynomial part of degree < p² - 1:

v_p^G(τ_X(g)) ≥ min_c (e_c - ℓ_c) - 4,

where e_c (resp. ℓ_c) is the number of zeros (resp. poles) in the class c mod p. This replaces the p-adic distribution formula of the paper (Lemmas 3.1–3.2).

noncomputable def Zeta5Irrational.numOf (κ : ℚ) (Z : Multiset ℤ) : Polynomial ℚ

The numerator κ ∏_{ζ ∈ Z} (x - ζ).

Equations

• Zeta5Irrational.numOf κ Z = Polynomial.C κ * (Multiset.map (fun (ζ : ℤ) => Polynomial.X - Polynomial.C ↑ζ) Z).prod

def Zeta5Irrational.cnt (p : ℕ) (Z : Multiset ℤ) (c : ZMod p) : ℕ

Number of zeros in the class c.

Equations

• Zeta5Irrational.cnt p Z c = (Multiset.filter (fun (ζ : ℤ) => ↑ζ = c) Z).card

def Zeta5Irrational.plc (p : ℕ) (Pl : Finset ℤ) (c : ZMod p) : Finset ℤ

Poles in the class c.

Equations

• Zeta5Irrational.plc p Pl c = {r ∈ Pl | ↑r = c}

Integer valuations

theorem Zeta5Irrational.zmod_eq_iff_dvd {p : ℕ} [hp : Fact (Nat.Prime p)] {a b : ℤ} : ↑a = ↑b ↔ ↑p ∣ a - b

theorem Zeta5Irrational.VG_int_one {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h : ↑p ∣ z) : VG p (↑z) 1

theorem Zeta5Irrational.padicValRat_int_eq_zero {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h : ¬↑p ∣ z) : padicValRat p ↑z = 0

theorem Zeta5Irrational.padicValRat_int_le_one {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ} (h2 : ¬↑p ^ 2 ∣ z) : padicValRat p ↑z ≤ 1

theorem Zeta5Irrational.padicValRat_finset_prod {p : ℕ} [hp : Fact (Nat.Prime p)] {ι : Type u_1} (s : Finset ι) (f : ι → ℚ) (hf : ∀ i ∈ s, f i ≠ 0) : padicValRat p (∏ i ∈ s, f i) = ∑ i ∈ s, padicValRat p (f i)

theorem Zeta5Irrational.VG.multiset_prod {p : ℕ} [hp : Fact (Nat.Prime p)] (s : Multiset ℚ) (b : ℚ → ℚ) (h : ∀ q ∈ s, VG p q (b q)) : VG p s.prod (Multiset.map b s).sum

The harmonic numbers

theorem Zeta5Irrational.VG_H5 {p : ℕ} [hp : Fact (Nat.Prime p)] {m : ℕ} (hm : m < p ^ 2) : VG p (H5 m) (-5)

Residues

theorem Zeta5Irrational.eval_numOf (κ : ℚ) (Z : Multiset ℤ) (x : ℚ) : Polynomial.eval x (numOf κ Z) = κ * (Multiset.map (fun (ζ : ℤ) => x - ↑ζ) Z).prod

theorem Zeta5Irrational.VG_prod_sub {p : ℕ} [hp : Fact (Nat.Prime p)] (Z : Multiset ℤ) (x : ℤ) : VG p (Multiset.map (fun (ζ : ℤ) => ↑x - ↑ζ) Z).prod ↑(cnt p Z ↑x)

theorem Zeta5Irrational.VG_eval_numOf {p : ℕ} [hp : Fact (Nat.Prime p)] (κ : ℚ) (hκ : VG p κ 0) (Z : Multiset ℤ) (x : ℤ) : VG p (Polynomial.eval (↑x) (numOf κ Z)) ↑(cnt p Z ↑x)

def Zeta5Irrational.Sep (p : ℕ) (Pl : Finset ℤ) : Prop

Poles in the same class differ by exactly one power of p.

Equations

• Zeta5Irrational.Sep p Pl = ∀ r ∈ Pl, ∀ s ∈ Pl, r ≠ s → ↑r = ↑s → ¬↑p ^ 2 ∣ r - s

theorem Zeta5Irrational.padicValRat_denom_le {p : ℕ} [hp : Fact (Nat.Prime p)] (Pl : Finset ℤ) (hsep : Sep p Pl) {r : ℤ} (hr : r ∈ Pl) : ↑(padicValRat p (∏ s ∈ Pl.erase r, (↑r - ↑s))) ≤ ↑(plc p Pl ↑r).card - 1

theorem Zeta5Irrational.VG_res {p : ℕ} [hp : Fact (Nat.Prime p)] (κ : ℚ) (hκ : VG p κ 0) (Z : Multiset ℤ) (Pl : Finset ℤ) (hsep : Sep p Pl) {r : ℤ} (hr : r ∈ Pl) : VG p (resP (numOf κ Z) Pl r) (↑(cnt p Z ↑r) - ↑(plc p Pl ↑r).card + 1)

Residue bound: v_p(res_r) ≥ e_c - ℓ_c + 1 for the class c of r.