Uniform bounds for the additive constants of the per-prime bounds

theorem Zeta5Irrational.abs_bcoef_le (h : ℕ → ℝ) {M : ℝ} (hM : ∀ a ≤ 2, |h a| ≤ M) (i : Fin 3) : |bcoef h i| ≤ 2 * M

theorem Zeta5Irrational.abs_bcoef2_le (h : ℕ → ℕ → ℝ) {M : ℝ} (hM : ∀ a ≤ 2, ∀ b ≤ 2, |h a b| ≤ M) (i j : Fin 3) : |bcoef (fun (a : ℕ) => bcoef (fun (b : ℕ) => h a b) j) i| ≤ 4 * M

theorem Zeta5Irrational.psiR_nonneg (k β : ℤ) : 0 ≤ psiR k β

theorem Zeta5Irrational.abs_psiR_le (k β : ℤ) : |↑(psiR k β)| ≤ ↑(k - β + 1) ^ 2

theorem Zeta5Irrational.sum_abs_bIn_le {q q' : ℕ} (hq' : q' ≤ q) {k : ℤ} (hk1 : -2 * ↑q - 6 ≤ k) (hk2 : k ≤ 8 * ↑q + 20) : ∑ i : Fin 3, ∑ j : Fin 3, |bIn q q' k i j| ≤ 36 * (22 * ↑q + 30) ^ 2

The inner coefficients.

theorem Zeta5Irrational.abs_GO_le (q a d : ℕ) : |↑(GO q a d)| ≤ (2 * ↑q + ↑a) * (↑q + ↑a + 3)

The outer coefficients.

theorem Zeta5Irrational.sum_abs_bGO_le {q : ℕ} (hq : q ≤ 2) : ∑ i : Fin 3, ∑ j : Fin 3, |bGO q i j| ≤ 36 * 70