Growth: the limits of the three prime sums

theorem Zeta5Irrational.aIn_le (i : ℕ) : i < 125 → |↑(aInL.getD i 0)| ≤ 100

theorem Zeta5Irrational.aOut_le (i : ℕ) : i < 13 → |↑(aOutL.getD i 0)| ≤ 100

theorem Zeta5Irrational.lin_lip (a b L : ℝ) (ha : |a| ≤ L) (x y : ℝ) : |a * x + b - (a * y + b)| ≤ L * |x - y|

theorem Zeta5Irrational.inner_psum_limit {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (K : ℝ) in Filter.atTop, psum fIn 3 20 K / K ^ 2 ≤ 322437603634266857629 / 7535670527041937280000 + δ

The inner table sum.

theorem Zeta5Irrational.tOut_zero : tOut 0 = 20 / 37

theorem Zeta5Irrational.tOut_last : tOut 13 = 3

theorem Zeta5Irrational.outer_psum_limit {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (K : ℝ) in Filter.atTop, psum Eout (20 / 37) 3 K / K ^ 2 ≤ 129101 / 96000 + δ

The outer table sum.

theorem Zeta5Irrational.tT_zero : tT 0 = 20

theorem Zeta5Irrational.tT_last : tT 1140 = 400

theorem Zeta5Irrational.qT_le_400 {i : ℕ} (hi : i < 1140) : ↑(qT i) ≤ 400

theorem Zeta5Irrational.qT'_le_30 {i : ℕ} (hi : i < 1140) : ↑(qT' i) ≤ 30

theorem Zeta5Irrational.tT_le_400 {i : ℕ} (hi : i ≤ 1140) : tT i ≤ 400

theorem Zeta5Irrational.tail_psum_limit {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (K : ℝ) in Filter.atTop, psum (fun (x : ℝ) => x * Ftail x + 27 / 16) 20 400 K / K ^ 2 ≤ -6843153 / 128000000 + δ

The tail sum.