The inner range in continuous form: -L_p ≤ p Ê(K/p, k) + C

Ê(x, k) = -2u⌊x⌋ + 12u⌊αx⌋ + 2J(u) - uk + 2 ∑_{i,j} b_{ij}(k) c_{ij}({x}, {αx}), with u = λx, the coefficients b_{ij} of the class function ψ(k, B + 6a' - a) in the basis 1, A, E, and the continuous interval counts c_{ij}.

noncomputable def Zeta5Irrational.bIn (q q' : ℕ) (k : ℤ) (i j : Fin 3) : ℝ

The class-function coefficients.

Equations

• Zeta5Irrational.bIn q q' k i j = Zeta5Irrational.bcoef (fun (a : ℕ) => Zeta5Irrational.bcoef (fun (b : ℕ) => ↑(Zeta5Irrational.psiR k (12 * ↑q' - 2 * ↑q - 4 + 6 * ↑b - ↑a))) j) i

noncomputable def Zeta5Irrational.Ein (x : ℝ) (k : ℤ) : ℝ

The continuous inner function.

Equations

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

noncomputable def Zeta5Irrational.Ctab (n p : ℕ) (k : ℤ) : ℝ

The additive error of the table bound.

Equations

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

theorem Zeta5Irrational.table_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) ≤ ↑p * Ein (40 * ↑n / ↑p) k + Ctab n p k

The inner bound in continuous form.