Small primes: the analogue of Lemma 3.3

For A integer-valued on ℤ with deg A ≤ d, 2K ≤ d: v_p^G(τ_X((K!)² A / ∏_{0<|r|≤K}(x - r))) ≥ -6 log_p (d+1) - v_p(24).

Instead of the paper's ball analysis we evaluate the polynomial part on the window K+1, …, d-K+1 beyond all poles, where (K!)²/∏(m - r) = 1/(C(m-1,K) C(m+K,K)), and use the window lemma.

theorem Zeta5Irrational.mem_PlK_iff {K : ℕ} {r : ℤ} (hr : r ∈ PlK K) : ∃ j ∈ Finset.Icc 1 K, ∃ (ε : ℤ), (ε = 1 ∨ ε = -1) ∧ r = ε * ↑j

theorem Zeta5Irrational.factorial_ratio {j K : ℕ} (hjK : j ≤ K) : ↑K.factorial ^ 2 / (↑(K - j).factorial * ↑(K + j).factorial) = ↑((2 * K).choose (K + j)) / ↑((2 * K).choose K)

(K!)² / ((K-j)! (K+j)!) = C(2K, K+j) / C(2K, K).

theorem Zeta5Irrational.VG_res_factor {p : ℕ} [hp : Fact (Nat.Prime p)] {K : ℕ} {r : ℤ} (hr : r ∈ PlK K) : VG p (↑K.factorial ^ 2 / ∏ s ∈ (PlK K).erase r, (↑r - ↑s)) (-↑(Nat.log p (2 * K)))

The residue factor (K!)² / ∏_{s ≠ r} (r - s) has valuation ≥ -log_p (2K).

theorem Zeta5Irrational.crude_tauX {p : ℕ} [hp : Fact (Nat.Prime p)] {K d : ℕ} (hK : 1 ≤ K) (hdK : 2 * K ≤ d) (A : Polynomial ℚ) (hA : A.natDegree ≤ d) (hint : ∀ (z : ℤ), VG p (Polynomial.eval (↑z) A) 0) : GV p (tauX (Polynomial.C (↑K.factorial ^ 2) * A) (PlK K)) (-6 * ↑(Nat.log p (d + 1)) - ↑(padicValNat p 24))

The analogue of Lemma 3.3 for the poles ±1, …, ±K.