The inner range: a per-prime upper bound for -L_p

For K/400 < p ≤ K/3 (and n large enough for the side conditions), every level k in [klo, ktop] gives -L_p ≤ -2h q + 12h q' + 2 T(h) - h k + 2 ∑_{c=1}^m ψ(k, B + 6a'_c - a_c) + (k - klo) L₀ + 2B₀ + 1, with q = ⌊K/p⌋, q' = ⌊N/p⌋, B = 12q' - 2q - 4, the class counts a_c, a'_c of ClassSum, and the layer-cake function T.

theorem Zeta5Irrational.sum_erase_zero_eq_Icc {m : ℕ} (F : ℕ → ℚ) : ∑ c ∈ Finset.univ.erase 0, F ↑c = ∑ c ∈ Finset.Icc 1 m, F c

theorem Zeta5Irrational.neg_vSK_le {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 1 ≤ n) (_hp3 : 3 ≤ p) (hN : 3 * n < p ^ 2) (hH : 2 * (37 * n) < p ^ 2) (J : ℕ) (hJ : 2 * (37 * n) ≤ J * p) : -↑(vSK n p) ≤ -2 * ↑(37 * n) * ↑(40 * n / p) + 12 * ↑(37 * n) * ↑(3 * n / p) + 2 * layer p J ↑(37 * n)

-v_p(S_K) in the inner and outer ranges.

noncomputable def Zeta5Irrational.Bmax (n p : ℕ) : ℝ

The zero-class deficit bound.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Zeta5Irrational.hIn (n p : ℕ) (k : ℤ) (a a' : ℕ) : ℝ

The class function of the inner range.

Equations

• Zeta5Irrational.hIn n p k a a' = ↑(Zeta5Irrational.psiR k (12 * ↑(3 * n / p) - 2 * ↑(40 * n / p) - 4 + 6 * ↑a' - ↑a))

theorem Zeta5Irrational.betaI_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hodd : 2 * (p / 2) + 1 = p) {c : ℕ} (hc1 : 1 ≤ c) (hcm : c ≤ p / 2) : betaI n p ⟨c, ⋯⟩ = 12 * ↑(3 * n / p) - 2 * ↑(40 * n / p) - 4 + 6 * ↑(aCnt p (3 * n % p) c) - ↑(aCnt p (40 * n % p) c)

theorem Zeta5Irrational.q_lt {p n : ℕ} (hodd : 2 * (p / 2) + 1 = p) (hsmall : ¬p * Mcut ≤ 40 * n) : 40 * n / p < 400

theorem Zeta5Irrational.klo_le_beta {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hodd : 2 * (p / 2) + 1 = p) (c : Fin (p / 2 + 1)) (hc : c ≠ 0) : kloI n p ≤ betaI n p c

theorem Zeta5Irrational.rowsK_klo {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hodd : 2 * (p / 2) + 1 = p) : rowsK (betaI n p) (kloI n p) = 0

theorem Zeta5Irrational.Bse_eq_beta {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (c : Fin (p / 2 + 1)) (hc : c ≠ 0) : Bse p (40 * n) (3 * n) ↑c = ↑(betaI n p c) + 4

theorem Zeta5Irrational.Bse_zero_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} : Bse p (40 * n) (3 * n) 0 = 5 + 12 * ↑(3 * n / p) - 2 * ↑(40 * n / p)

theorem Zeta5Irrational.innerOK_of {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 33 ≤ n) (hodd : 2 * (p / 2) + 1 = p) (hp7 : 7 ≤ p) (hsmall : ¬p * Mcut ≤ 40 * n) (hin : 3 * p ≤ 40 * n) (hsq : 2 * (40 * n) < p ^ 2) (hdeg : 5 + 2 * (18 * n + 2 * (37 * n)) - 2 * (40 * n) + 1 < p ^ 2) : InnerOK n p

The inner side conditions hold.

theorem Zeta5Irrational.inner_Lp_le {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} (hn : 33 ≤ n) (hodd : 2 * (p / 2) + 1 = p) (hp7 : 7 ≤ p) (hsmall : ¬p * Mcut ≤ 40 * n) (hin : 3 * p ≤ 40 * n) (hsq : 2 * (40 * n) < p ^ 2) (hdeg : 5 + 2 * (18 * n + 2 * (37 * n)) - 2 * (40 * n) + 1 < p ^ 2) (k : ℤ) (hk1 : kloI n p ≤ k) (hk2 : k ≤ ktopI n p) : -↑(Lp n p) ≤ -2 * ↑(37 * n) * ↑(40 * n / p) + 12 * ↑(37 * n) * ↑(3 * n / p) + 2 * layer p 1000 ↑(37 * n) - ↑(37 * n) * ↑k + 2 * ∑ c ∈ Finset.Icc 1 (p / 2), hIn n p k (aCnt p (40 * n % p) c) (aCnt p (3 * n % p) c) + ↑(k - kloI n p) * ↑(L0I n p) + 2 * Bmax n p + 1

The inner per-prime bound (discrete form).