Growth: decomposition of log m_K and the small primes

theorem Zeta5Irrational.log_mN (n : ℕ) : Real.log ↑(mN n) = ∑ k ∈ Finset.Icc 1 (2 * (37 * n)), cPrime k * -↑(Lp n k)

log m_K = ∑_{k ≤ 2h} c(k) (-L_k).

theorem Zeta5Irrational.sum_split4 (F : ℕ → ℝ) {a b c N : ℕ} (hab : a ≤ b) (hbc : b ≤ c) (hcN : c ≤ N) : ∑ k ∈ Finset.Icc 1 N, F k = ∑ k ∈ Finset.Ioc 0 a, F k + ∑ k ∈ Finset.Ioc a b, F k + ∑ k ∈ Finset.Ioc b c, F k + ∑ k ∈ Finset.Ioc c N, F k

Splitting (0, N] at a ≤ b ≤ c.

Small primes

theorem Zeta5Irrational.log_mul_natLog_le {k Z : ℕ} (hk : 2 ≤ k) (hZ : 1 ≤ Z) : ↑(Nat.log k Z) * Real.log ↑k ≤ Real.log ↑Z

theorem Zeta5Irrational.cPrime_natLog_le {k Z : ℕ} (hZ : 1 ≤ Z) : cPrime k * ↑(Nat.log k Z) ≤ cPrime k + if k * k ≤ Z then Real.log ↑Z else 0

theorem Zeta5Irrational.sum_cPrime_le_theta (M : ℕ) : ∑ k ∈ Finset.Ioc 0 M, cPrime k ≤ Chebyshev.theta ↑M

theorem Zeta5Irrational.cPrime_nonneg' (k : ℕ) : 0 ≤ cPrime k

theorem Zeta5Irrational.small_range_le (n : ℕ) (hn : 1 ≤ n) : ∑ k ∈ Finset.Ioc 0 (n / 10), cPrime k * -↑(Lp n k) ≤ 6 * (37 * ↑n) * (Chebyshev.theta ↑(n / 10) + (√(200 * ↑n) + 1) * Real.log (200 * ↑n)) + 37 * ↑n * 100

The small-prime range.