Small primes: generic tools for the bound (3.12)

• integer values of the binomial polynomials at all integers;
• a polynomial of degree ≤ d whose values at d + 1 consecutive integers have valuation ≥ β has valuation ≥ β at every integer (VG_eval_int_of_window);
• Kummer's bound v_p(C(n, k)) ≤ log_p n;
• v_p(H^{(5)}_m) ≥ -5 log_p m.

theorem Zeta5Irrational.bin_eval_int (k : ℕ) (z : ℤ) : ∃ (w : ℤ), Polynomial.eval (↑z) (bin k) = ↑w

Values of bin k at integers are integers.

theorem Zeta5Irrational.VG_bin_eval_int {p : ℕ} (k : ℕ) (z : ℤ) : VG p (Polynomial.eval (↑z) (bin k)) 0

theorem Zeta5Irrational.VG_eval_int_of_window {p : ℕ} [hp : Fact (Nat.Prime p)] {P : Polynomial ℚ} {d : ℕ} (hd : P.natDegree ≤ d) (s : ℤ) {β : ℚ} (hv : ∀ i ≤ d, VG p (Polynomial.eval (↑(s + ↑i)) P) β) (z : ℤ) : VG p (Polynomial.eval (↑z) P) β

Window lemma: values at s, …, s + d control the values at all integers.

theorem Zeta5Irrational.VG_choose_inv {p : ℕ} [hp : Fact (Nat.Prime p)] {n k : ℕ} (hk : k ≤ n) : VG p (↑(n.choose k))⁻¹ (-↑(Nat.log p n))

Kummer: v_p(C(n, k)⁻¹) ≥ -log_p n.

theorem Zeta5Irrational.VG_H5_log {p : ℕ} [hp : Fact (Nat.Prime p)] (m : ℕ) : VG p (H5 m) (-5 * ↑(Nat.log p m))

v_p(H^{(5)}_m) ≥ -5 log_p m.

theorem Zeta5Irrational.log_mono {p a b : ℕ} (h : a ≤ b) : ↑(Nat.log p a) ≤ ↑(Nat.log p b)