Growth: the per-range sums as prime sums

theorem Zeta5Irrational.range_sum_le {a b : ℕ} (F : ℕ → ℝ) (f : ℝ → ℝ) (K C : ℝ) (hC : 0 ≤ C) (h : ∀ k ∈ Finset.Ioc a b, Nat.Prime k → F k ≤ ↑k * f (K / ↑k) + C) : ∑ k ∈ Finset.Ioc a b, cPrime k * F k ≤ ∑ k ∈ Finset.Ioc a b, ↑k * cPrime k * f (K / ↑k) + C * Chebyshev.theta ↑b

theorem Zeta5Irrational.big_prime_facts {n k : ℕ} (hn : 10400 ≤ n) (hk : n / 10 < k) (hp : Nat.Prime k) : 7 ≤ k ∧ 2 * (k / 2) + 1 = k ∧ ¬k * Mcut ≤ 40 * n ∧ 2 * (40 * n) < k ^ 2 ∧ 5 + 2 * (18 * n + 2 * (37 * n)) - 2 * (40 * n) + 1 < k ^ 2 ∧ ↑n ≤ 10 * ↑k

Facts about primes above n/10 for large n.

theorem Zeta5Irrational.range2_le {n : ℕ} (hn : 10400 ≤ n) : ∑ k ∈ Finset.Ioc (n / 10) (2 * n), cPrime k * -↑(Lp n k) ≤ psum (fun (x : ℝ) => x * Ftail x + 27 / 16) 20 400 (Kr n) + 10 ^ 7 * Chebyshev.theta ↑(2 * n)

Range 2 (inner tail).

noncomputable def Zeta5Irrational.fIn (x : ℝ) : ℝ

The inner table as a function.

Equations

• Zeta5Irrational.fIn x = Zeta5Irrational.gIn (Zeta5Irrational.pieceIdx Zeta5Irrational.tIn 125 x) x

theorem Zeta5Irrational.tIn_zero : tIn 0 = 3

theorem Zeta5Irrational.tIn_last : tIn 125 = 20

theorem Zeta5Irrational.range3_le {n : ℕ} (hn : 10400 ≤ n) : ∑ k ∈ Finset.Ioc (2 * n) (40 * n / 3), cPrime k * -↑(Lp n k) ≤ psum fIn 3 20 (Kr n) + 10 ^ 8 * Chebyshev.theta ↑(40 * n / 3)

Range 3 (inner table).

theorem Zeta5Irrational.range4_le {n : ℕ} (hn : 10400 ≤ n) : ∑ k ∈ Finset.Ioc (40 * n / 3) (2 * (37 * n)), cPrime k * -↑(Lp n k) ≤ psum Eout (20 / 37) 3 (Kr n) + 10 ^ 5 * Chebyshev.theta ↑(2 * (37 * n))

Range 4 (outer range).