arith_sum: the prime sum behind the arithmetic constant (the proof notes, §8, the proof notes, §8.5, finite-piece route).

The primes p ≤ 5n are split as

• p ≤ n/20: p ≤ n^{2/3} by the crude bound h0 (total o(n²)), n^{2/3} < p ≤ n/20 by h1 and psiL x ≤ tailConst on x ≤ 1/20, total tailConst · n · θ(n/20);
• n/20 < p ≤ 7n/3: h1, and on each of the 196 pieces n psiL(p/n) = a n + b p − (25/4) n²/p;
• 7n/3 < p ≤ 5n: h2, four linear pieces of phiL;
• the additive constants 3/4 and 5 cost at most (13/2) θ(5n) = O(n). The normalised main part tends to tailConst/20 + midRat + 35/36 − (25/4) log(140/3) < 283/50.

Real piece data

def Zeta32.ArithSum.tR (i : ℕ) : ℝ

Real breakpoint for the relaxed arithmetic profile.

Equations

• Zeta32.ArithSum.tR i = ↑(Zeta32.ArithSum.ub i)

def Zeta32.ArithSum.tO (i : ℕ) : ℝ

Real breakpoint for the outer-prime profile.

Equations

• Zeta32.ArithSum.tO i = ↑(Zeta32.ArithSum.vb i)

theorem Zeta32.ArithSum.tR_pos (i : ℕ) : 0 < tR i

theorem Zeta32.ArithSum.tR_lt (i : ℕ) : tR i < tR (i + 1)

theorem Zeta32.ArithSum.tR_zero : tR 0 = 3 / 7

theorem Zeta32.ArithSum.tR_196 : tR 196 = 20

theorem Zeta32.ArithSum.tO_zero : tO 0 = 1 / 5

theorem Zeta32.ArithSum.tO_four : tO 4 = 3 / 7

theorem Zeta32.ArithSum.tO_pos (i : ℕ) : 0 < tO i

theorem Zeta32.ArithSum.tO_lt (i : ℕ) (hi : i < 4) : tO i < tO (i + 1)

theorem Zeta32.ArithSum.floor_bounds {n k : ℕ} {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hk : k ∈ Finset.Ioc ⌊↑n / t⌋₊ ⌊↑n / s⌋₊) : 0 < k ∧ s ≤ ↑n / ↑k ∧ ↑n / ↑k < t

The three limits

theorem Zeta32.ArithSum.relaxed_tendsto : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Ioc ⌊↑n / 20⌋₊ ⌊↑n / (3 / 7)⌋₊, ↑n * psiL (↑k / ↑n) * Zeta5Irrational.cPrime k) / ↑n ^ 2) Filter.atTop (nhds (↑midRat - 25 / 4 * Real.log (140 / 3)))

theorem Zeta32.ArithSum.outer_tendsto : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Ioc ⌊↑n / (3 / 7)⌋₊ ⌊↑n / (1 / 5)⌋₊, ↑n * phiL (↑k / ↑n) * Zeta5Irrational.cPrime k) / ↑n ^ 2) Filter.atTop (nhds (35 / 36))

theorem Zeta32.ArithSum.tail_tendsto : Filter.Tendsto (fun (n : ℕ) => ↑tailConst * ↑n * Chebyshev.theta (↑n / 20) / ↑n ^ 2) Filter.atTop (nhds (↑tailConst / 20))

Elementary bounds

theorem Zeta32.ArithSum.cPrime_log_eq {k : ℕ} (hk : Nat.Prime k) : Zeta5Irrational.cPrime k = Real.log ↑k

theorem Zeta32.ArithSum.cPrime_zero_of {k : ℕ} (hk : ¬Nat.Prime k) : Zeta5Irrational.cPrime k = 0

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

theorem Zeta32.ArithSum.padicValNat_mul_log_le {k d : ℕ} (hk : Nat.Prime k) (hd : 0 < d) : ↑(padicValNat k d) * Real.log ↑k ≤ Real.log ↑d

theorem Zeta32.ArithSum.sum_ite_le (M : ℕ) {y B : ℝ} (hy : 0 ≤ y) (hB : 0 ≤ B) : (∑ k ∈ Finset.Ioc 0 M, if ↑k ≤ y then B else 0) ≤ y * B

theorem Zeta32.ArithSum.sum_filter_prime_eq (F : ℕ → ℝ) (N : ℕ) : ∑ p ∈ Finset.range (N + 1) with Nat.Prime p, F p * Real.log ↑p = ∑ k ∈ Finset.Ioc 0 N, F k * Zeta5Irrational.cPrime k

theorem Zeta32.ArithSum.sum_cPrime_le {a b c : ℕ} (hbc : b ≤ c) : ∑ k ∈ Finset.Ioc a b, Zeta5Irrational.cPrime k ≤ ∑ k ∈ Finset.Ioc 0 c, Zeta5Irrational.cPrime k

theorem Zeta32.ArithSum.rpow_facts (δ C : ℝ) (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (2 / 3) ≤ ↑n / 20 ∧ ↑n ^ (2 / 3) * (9 * ↑n * Real.log (10 * ↑n + 2) + 3 * ↑n * C) ≤ δ * ↑n ^ 2

n^{2/3} ≤ n/20 and the crude small-prime total is ≤ δ n², eventually.

The three ranges at a fixed n

theorem Zeta32.ArithSum.tail_range_bound (cost : ℕ → ℕ → ℝ) (den : ℕ) (hden : 0 < den) (n : ℕ) (h0 : ∀ (p : ℕ), Nat.Prime p → cost n p ≤ 9 * ↑n * ↑(Nat.log p (10 * n + 2)) + 3 * ↑n * ↑(padicValNat p den)) (hh1 : ∀ (p : ℕ), Nat.Prime p → ↑n ^ (2 / 3) < ↑p → 3 * p ≤ 7 * n → cost n p ≤ ↑n * psiL (↑p / ↑n) + 3 / 4) : ∑ k ∈ Finset.Ioc 0 ⌊↑n / 20⌋₊, cost n k * Zeta5Irrational.cPrime k ≤ (↑n * ↑tailConst + 3 / 4) * Chebyshev.theta (↑n / 20) + ↑n ^ (2 / 3) * (9 * ↑n * Real.log (10 * ↑n + 2) + 3 * ↑n * Real.log ↑den)

theorem Zeta32.ArithSum.relaxed_range_bound (cost : ℕ → ℕ → ℝ) (n : ℕ) (hpow : ↑n ^ (2 / 3) ≤ ↑n / 20) (hh1 : ∀ (p : ℕ), Nat.Prime p → ↑n ^ (2 / 3) < ↑p → 3 * p ≤ 7 * n → cost n p ≤ ↑n * psiL (↑p / ↑n) + 3 / 4) : ∑ k ∈ Finset.Ioc ⌊↑n / 20⌋₊ ⌊↑n / (3 / 7)⌋₊, cost n k * Zeta5Irrational.cPrime k ≤ ∑ k ∈ Finset.Ioc ⌊↑n / 20⌋₊ ⌊↑n / (3 / 7)⌋₊, ↑n * psiL (↑k / ↑n) * Zeta5Irrational.cPrime k + 3 / 4 * ∑ k ∈ Finset.Ioc ⌊↑n / 20⌋₊ ⌊↑n / (3 / 7)⌋₊, Zeta5Irrational.cPrime k

theorem Zeta32.ArithSum.outer_range_bound (cost : ℕ → ℕ → ℝ) (n : ℕ) (hh2 : ∀ (p : ℕ), Nat.Prime p → 7 * n < 3 * p → p ≤ 5 * n → cost n p ≤ ↑n * phiL (↑p / ↑n) + 5) : ∑ k ∈ Finset.Ioc ⌊↑n / (3 / 7)⌋₊ ⌊↑n / (1 / 5)⌋₊, cost n k * Zeta5Irrational.cPrime k ≤ ∑ k ∈ Finset.Ioc ⌊↑n / (3 / 7)⌋₊ ⌊↑n / (1 / 5)⌋₊, ↑n * phiL (↑k / ↑n) * Zeta5Irrational.cPrime k + 5 * ∑ k ∈ Finset.Ioc ⌊↑n / (3 / 7)⌋₊ ⌊↑n / (1 / 5)⌋₊, Zeta5Irrational.cPrime k

The theorem

theorem Zeta32.ArithSum.arith_sum (cost : ℕ → ℕ → ℝ) (den : ℕ) (hden : 0 < den) (h0 : ∀ (n p : ℕ), Nat.Prime p → cost n p ≤ 9 * ↑n * ↑(Nat.log p (10 * n + 2)) + 3 * ↑n * ↑(padicValNat p den)) (h1 : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ), Nat.Prime p → ↑n ^ (2 / 3) < ↑p → 3 * p ≤ 7 * n → cost n p ≤ ↑n * psiL (↑p / ↑n) + 3 / 4) (h2 : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : ℕ), Nat.Prime p → 7 * n < 3 * p → p ≤ 5 * n → cost n p ≤ ↑n * phiL (↑p / ↑n) + 5) (ε : ℝ) : ε > 0 → ∀ᶠ (n : ℕ) in Filter.atTop, ∑ p ∈ Finset.range (5 * n + 1) with Nat.Prime p, cost n p * Real.log ↑p ≤ (283 / 50 + ε) * ↑n ^ 2