Prime sums with a weight function

psum f a b K = ∑_{K/b < p ≤ K/a} p f(K/p) log p. If f ≤ v_j on each cell [c_j, c_{j+1}] of a partition a = c_0 < ⋯ < c_r = b, then psum f a b K ≤ ∑_j v_j wsum (K/c_{j+1}) (K/c_j), and the right-hand side is K² ∑_j v_j (1/c_j² - 1/c_{j+1}²)/2 + o(K²).

noncomputable def Zeta5Irrational.psum (f : ℝ → ℝ) (a b K : ℝ) : ℝ

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

Equations

• Zeta5Irrational.psum f a b K = ∑ k ∈ Finset.Ioc ⌊K / b⌋₊ ⌊K / a⌋₊, ↑k * Zeta5Irrational.cPrime k * f (K / ↑k)

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

theorem Zeta5Irrational.psum_split (f : ℝ → ℝ) {a c b K : ℝ} (ha : 0 < a) (hac : a ≤ c) (hcb : c ≤ b) (hK : 0 ≤ K) : psum f a b K = psum f a c K + psum f c b K

Splitting at an intermediate point.

theorem Zeta5Irrational.psum_le_of_le {f : ℝ → ℝ} {a b v K : ℝ} (ha : 0 < a) (hab : a ≤ b) (hK : 0 < K) (hf : ∀ x ∈ Set.Ico a b, f x ≤ v) : psum f a b K ≤ v * wsum (K / b) (K / a)

If f ≤ v on [a, b), then psum f a b K ≤ v * wsum (K/b) (K/a).

noncomputable def Zeta5Irrational.stepSum (c v : ℕ → ℝ) (r : ℕ) (K : ℝ) : ℝ

The step sum over a partition c 0 < c 1 < ⋯ < c r, with values v j on [c j, c (j+1)].

Equations

• Zeta5Irrational.stepSum c v r K = ∑ j ∈ Finset.range r, v j * Zeta5Irrational.wsum (K / c (j + 1)) (K / c j)

theorem Zeta5Irrational.c_zero_le {c : ℕ → ℝ} {r : ℕ} (h : ∀ j < r, c j ≤ c (j + 1)) : c 0 ≤ c r

theorem Zeta5Irrational.psum_le_stepSum {f : ℝ → ℝ} {c v : ℕ → ℝ} (r : ℕ) (hc0 : 0 < c 0) (hmono : ∀ j < r, c j ≤ c (j + 1)) (hf : ∀ j < r, ∀ x ∈ Set.Ico (c j) (c (j + 1)), f x ≤ v j) {K : ℝ} (hK : 0 < K) : psum f (c 0) (c r) K ≤ stepSum c v r K

Upper bound of psum over a partition by the step sum.

theorem Zeta5Irrational.stepSum_tendsto {c v : ℕ → ℝ} (r : ℕ) (hc0 : 0 < c 0) (hmono : ∀ j < r, c j < c (j + 1)) : Filter.Tendsto (fun (K : ℝ) => stepSum c v r K / K ^ 2) Filter.atTop (nhds (∑ j ∈ Finset.range r, v j * ((1 / c j ^ 2 - 1 / c (j + 1) ^ 2) / 2)))

The limit of the normalised step sum.

theorem Zeta5Irrational.psum_eventually_le {f : ℝ → ℝ} {c v : ℕ → ℝ} (r : ℕ) (hc0 : 0 < c 0) (hmono : ∀ j < r, c j < c (j + 1)) (hf : ∀ j < r, ∀ x ∈ Set.Ico (c j) (c (j + 1)), f x ≤ v j) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (K : ℝ) in Filter.atTop, psum f (c 0) (c r) K / K ^ 2 ≤ ∑ j ∈ Finset.range r, v j * ((1 / c j ^ 2 - 1 / c (j + 1) ^ 2) / 2) + ε

Eventually, psum f a b K / K² ≤ (upper Darboux sum) + ε.