Small primes: the bound (3.12)

v_p^G(F_K) ≥ -6h ⌊log_p (5K)⌋ - h v_p(24) for every prime p (small_prime_bound), via the basis q_0 = 1, q_i(t) = (-1)^i 2t D_{i-1}(t)/(2i)! with q_i(-z²) = C(z+i, 2i) + C(z+i-1, 2i).

noncomputable def Zeta5Irrational.qP (a : ℕ) : Polynomial ℚ

The basis q_a.

Equations

• Zeta5Irrational.qP a = if a = 0 then 1 else Polynomial.C ((-1) ^ a * 2 / ↑(2 * a).factorial) * (Polynomial.X * Zeta5Irrational.D (a - 1))

noncomputable def Zeta5Irrational.qlead (a : ℕ) : ℚ

Its leading coefficient.

Equations

• Zeta5Irrational.qlead a = if a = 0 then 1 else (-1) ^ a * 2 / ↑(2 * a).factorial

theorem Zeta5Irrational.qlead_ne_zero (a : ℕ) : qlead a ≠ 0

theorem Zeta5Irrational.qP_eq (a : ℕ) : qP a = Polynomial.C (qlead a) * if a = 0 then 1 else Polynomial.X * D (a - 1)

theorem Zeta5Irrational.monic_qbase (a : ℕ) : (if a = 0 then 1 else Polynomial.X * D (a - 1)).Monic

theorem Zeta5Irrational.natDegree_qbase (a : ℕ) : (if a = 0 then 1 else Polynomial.X * D (a - 1)).natDegree = a

theorem Zeta5Irrational.natDegree_qP (a : ℕ) : (qP a).natDegree = a

theorem Zeta5Irrational.coeff_qP_self (a : ℕ) : (qP a).coeff a = qlead a

Integer values

theorem Zeta5Irrational.prod_Icc_eq_prod_range (N : ℕ) (g : ℕ → ℚ) : ∏ j ∈ Finset.Icc 1 N, g j = ∏ i ∈ Finset.range N, g (i + 1)

theorem Zeta5Irrational.bin_eval_eq (k : ℕ) (y : ℚ) : Polynomial.eval y (bin k) = (∏ i ∈ Finset.range k, (y - ↑i)) / ↑k.factorial

theorem Zeta5Irrational.prod_window (z : ℚ) (c : ℕ) : ∏ i ∈ Finset.range (2 * c + 1), (z + ↑c - ↑i) = z * ∏ j ∈ Finset.Icc 1 c, (z ^ 2 - ↑j ^ 2)

∏_{i < 2c+1} (z + c - i) = z ∏_{j ≤ c} (z² - j²).

theorem Zeta5Irrational.qP_eval_neg_sq {a : ℕ} (ha : 1 ≤ a) (z : ℚ) : Polynomial.eval (-z ^ 2) (qP a) = Polynomial.eval (z + ↑a) (bin (2 * a)) + Polynomial.eval (z + ↑a - 1) (bin (2 * a))

q_a(-z²) = C(z+a, 2a) + C(z+a-1, 2a) for a ≥ 1.

theorem Zeta5Irrational.VG_qP_eval {p : ℕ} [hp : Fact (Nat.Prime p)] (a : ℕ) (z : ℤ) : VG p (Polynomial.eval (-↑z ^ 2) (qP a)) 0

theorem Zeta5Irrational.D_eval_neg_sq (N : ℕ) (z : ℚ) : Polynomial.eval (-z ^ 2) (D N) = ↑N.factorial ^ 2 * (Polynomial.eval (↑N + z) (bin N) * Polynomial.eval (↑N - z) (bin N))

D_N(-z²) = (N!)² C(N+z, N) C(N-z, N).

theorem Zeta5Irrational.VG_D_eval {p : ℕ} [hp : Fact (Nat.Prime p)] (N : ℕ) (z : ℤ) : VG p (Polynomial.eval (-↑z ^ 2) (D N) / ↑N.factorial ^ 2) 0

Assembly

theorem Zeta5Irrational.det_coeffMat_qP (h : ℕ) : (coeffMat fun (a : Fin h) => qP ↑a).det = ∏ a : Fin h, qlead ↑a

theorem Zeta5Irrational.qlead_sq {a : ℕ} (ha : 1 ≤ a) : qlead a ^ 2 = 4 / ↑(2 * a).factorial ^ 2

theorem Zeta5Irrational.prod_qlead_sq (h : ℕ) (hh : 1 ≤ h) : (∏ a : Fin h, qlead ↑a) ^ 2 = 4 ^ (h - 1) / ∏ i ∈ Finset.Icc 1 (h - 1), ↑(2 * i).factorial ^ 2

theorem Zeta5Irrational.S_eq_qlead (n : ℕ) (hn : 1 ≤ n) : S n = (↑(40 * n).factorial ^ 2 / ↑(3 * n).factorial ^ 12) ^ (37 * n) * (∏ a : Fin (37 * n), qlead ↑a) ^ 2

S_K = ((K!)²/(N!)¹²)^h det(C)².

theorem Zeta5Irrational.small_prime_bound {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) : GV p (F n) (-(6 * ↑(37 * n) * ↑(Nat.log p (200 * n)) + ↑(37 * n) * ↑(padicValNat p 24)))

The bound (3.12) at every prime.