Prime sums over windows n/u₂ < p ≤ n/u₁ (the proof notes, §8.5, Lemma 11), in the parametrisation u = n/p.

• logSum (n/u₂) (n/u₁) / n → 1/u₁ − 1/u₂ (θ(y) ~ y)
• wsum (n/u₂) (n/u₁) / n² → (1/u₁² − 1/u₂²)/2 (Abel summation with f(t) = t)
• lsum (n/u₂) (n/u₁) → log (u₂/u₁) (Abel summation with f(t) = 1/t)

and the resulting limit of one "piece" ∑ (A n + B p + C n²/p) log p, plus the splitting of a window into consecutive pieces.

noncomputable def Zeta32.ArithSum.PrimeSums.lsum (a b : ℝ) : ℝ

∑_{a < p ≤ b} (log p)/p.

Equations

• Zeta32.ArithSum.PrimeSums.lsum a b = ∑ k ∈ Finset.Ioc ⌊a⌋₊ ⌊b⌋₊, (↑k)⁻¹ * Zeta5Irrational.cPrime k

theorem Zeta32.ArithSum.PrimeSums.cPrime_nonneg (k : ℕ) : 0 ≤ cPrime k

Abel summation for f(t) = 1/t

theorem Zeta32.ArithSum.PrimeSums.lsum_eq {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : lsum a b = b⁻¹ * Chebyshev.theta b - a⁻¹ * Chebyshev.theta a - ∫ (t : ℝ) in Set.Ioc a b, deriv (fun (t : ℝ) => t⁻¹) t * Chebyshev.theta t

theorem Zeta32.ArithSum.PrimeSums.lsum_close {a b η : ℝ} (ha : 0 < a) (hab : a ≤ b) (h : ∀ y ∈ Set.Icc a b, |Chebyshev.theta y - y| ≤ η * y) : |lsum a b - Real.log (b / a)| ≤ η * (2 + Real.log (b / a))

Window limits in the parametrisation u = n/p

theorem Zeta32.ArithSum.PrimeSums.lsum_tendsto {c d : ℝ} (hc : 0 < c) (hcd : c ≤ d) : Filter.Tendsto (fun (K : ℝ) => lsum (K / d) (K / c)) Filter.atTop (nhds (Real.log (d / c)))

theorem Zeta32.ArithSum.PrimeSums.logSum_tendsto {c d : ℝ} (hc : 0 < c) (hcd : c ≤ d) : Filter.Tendsto (fun (K : ℝ) => logSum (K / d) (K / c) / K) Filter.atTop (nhds (1 / c - 1 / d))

One piece

noncomputable def Zeta32.ArithSum.PrimeSums.pieceSum (A B C u₁ u₂ : ℝ) (n : ℕ) : ℝ

∑_{n/u₂ < p ≤ n/u₁} (A n + B p + C n²/p) log p.

Equations

• Zeta32.ArithSum.PrimeSums.pieceSum A B C u₁ u₂ n = ∑ k ∈ Finset.Ioc ⌊↑n / u₂⌋₊ ⌊↑n / u₁⌋₊, (A * ↑n + B * ↑k + C * ↑n ^ 2 / ↑k) * Zeta5Irrational.cPrime k

noncomputable def Zeta32.ArithSum.PrimeSums.pieceLim (A B C u₁ u₂ : ℝ) : ℝ

The normalised limit of one piece.

Equations

• Zeta32.ArithSum.PrimeSums.pieceLim A B C u₁ u₂ = A * (1 / u₁ - 1 / u₂) + B * ((1 / u₁ ^ 2 - 1 / u₂ ^ 2) / 2) + C * Real.log (u₂ / u₁)

theorem Zeta32.ArithSum.PrimeSums.pieceSum_eq (A B C u₁ u₂ : ℝ) (n : ℕ) : pieceSum A B C u₁ u₂ n = A * ↑n * logSum (↑n / u₂) (↑n / u₁) + B * wsum (↑n / u₂) (↑n / u₁) + C * ↑n ^ 2 * lsum (↑n / u₂) (↑n / u₁)

theorem Zeta32.ArithSum.PrimeSums.pieceSum_tendsto (A B C : ℝ) {u₁ u₂ : ℝ} (hu₁ : 0 < u₁) (hu : u₁ < u₂) : Filter.Tendsto (fun (n : ℕ) => pieceSum A B C u₁ u₂ n / ↑n ^ 2) Filter.atTop (nhds (pieceLim A B C u₁ u₂))

Splitting a window into consecutive pieces

theorem Zeta32.ArithSum.PrimeSums.floor_div_anti {x s t : ℝ} (hx : 0 ≤ x) (hs : 0 < s) (hst : s ≤ t) : ⌊x / t⌋₊ ≤ ⌊x / s⌋₊

theorem Zeta32.ArithSum.PrimeSums.sum_split_pieces (F t : ℕ → ℝ) (x : ℝ) (hx : 0 ≤ x) (ht0 : 0 < t 0) (N : ℕ) : (∀ i < N, t i ≤ t (i + 1)) → ∑ k ∈ Finset.Ioc ⌊x / t N⌋₊ ⌊x / t 0⌋₊, F k = ∑ i ∈ Finset.range N, ∑ k ∈ Finset.Ioc ⌊x / t (i + 1)⌋₊ ⌊x / t i⌋₊, F k

theorem Zeta32.ArithSum.PrimeSums.window_tendsto (f : ℕ → ℕ → ℝ) (t A B C : ℕ → ℝ) (N : ℕ) (ht0 : 0 < t 0) (hmono : ∀ i < N, t i < t (i + 1)) (hf : ∀ (n : ℕ), 0 < n → ∀ i < N, ∀ k ∈ Finset.Ioc ⌊↑n / t (i + 1)⌋₊ ⌊↑n / t i⌋₊, f n k * cPrime k = (A i * ↑n + B i * ↑k + C i * ↑n ^ 2 / ↑k) * cPrime k) : Filter.Tendsto (fun (n : ℕ) => (∑ k ∈ Finset.Ioc ⌊↑n / t N⌋₊ ⌊↑n / t 0⌋₊, f n k * cPrime k) / ↑n ^ 2) Filter.atTop (nhds (∑ i ∈ Finset.range N, pieceLim (A i) (B i) (C i) (t i) (t (i + 1))))

If the summand agrees on piece i with (A i) n + (B i) k + (C i) n²/k (times cPrime k), the window sum is the sum of the pieces, and its normalised limit is the sum of the piece limits.