Prime sums and integrals

For f Lipschitz on [a, b] (0 < a < b), psum f a b K / K² ≤ ∫_a^b f(x)/x³ dx + ε for all large K; and the piecewise version for f given by Lipschitz pieces on [t_i, t_{i+1}).

theorem Zeta5Irrational.integral_inv_cube {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ∫ (x : ℝ) in a..b, x ^ (-3) = (1 / a ^ 2 - 1 / b ^ 2) / 2

theorem Zeta5Irrational.psum_le_integral {f : ℝ → ℝ} {a b L : ℝ} (ha : 0 < a) (hab : a < b) (hL : 0 ≤ L) (hcont : ContinuousOn f (Set.Icc a b)) (hLip : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ L * |x - y|) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (K : ℝ) in Filter.atTop, psum f a b K / K ^ 2 ≤ (∫ (x : ℝ) in a..b, f x / x ^ 3) + ε

Upper bound for psum by the integral, for f Lipschitz on [a, b].

theorem Zeta5Irrational.div_mem_Ico {a b K : ℝ} (ha : 0 < a) (hab : a ≤ b) (hK : 0 < K) {k : ℕ} (hk : k ∈ Finset.Ioc ⌊K / b⌋₊ ⌊K / a⌋₊) : K / ↑k ∈ Set.Ico a b

K/k ∈ [a, b) for k ∈ Ioc ⌊K/b⌋₊ ⌊K/a⌋₊.

theorem Zeta5Irrational.psum_congr {f g : ℝ → ℝ} {a b K : ℝ} (ha : 0 < a) (hab : a ≤ b) (hK : 0 < K) (h : ∀ x ∈ Set.Ico a b, f x = g x) : psum f a b K = psum g a b K

theorem Zeta5Irrational.psum_sum_split (f : ℝ → ℝ) {t : ℕ → ℝ} (m : ℕ) (ht0 : 0 < t 0) (hmono : ∀ i < m, t i ≤ t (i + 1)) {K : ℝ} (hK : 0 ≤ K) : psum f (t 0) (t m) K = ∑ i ∈ Finset.range m, psum f (t i) (t (i + 1)) K

theorem Zeta5Irrational.psum_piecewise_le {f : ℝ → ℝ} {g : ℕ → ℝ → ℝ} {t : ℕ → ℝ} {L : ℝ} (m : ℕ) (ht0 : 0 < t 0) (hmono : ∀ i < m, t i < t (i + 1)) (hL : 0 ≤ L) (hcont : ∀ i < m, ContinuousOn (g i) (Set.Icc (t i) (t (i + 1)))) (hLip : ∀ i < m, ∀ x ∈ Set.Icc (t i) (t (i + 1)), ∀ y ∈ Set.Icc (t i) (t (i + 1)), |g i x - g i y| ≤ L * |x - y|) (hfg : ∀ i < m, ∀ x ∈ Set.Ico (t i) (t (i + 1)), f x = g i x) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (K : ℝ) in Filter.atTop, psum f (t 0) (t m) K / K ^ 2 ≤ (∑ i ∈ Finset.range m, ∫ (x : ℝ) in t i..t (i + 1), g i x / x ^ 3) + ε

The piecewise version: f = g i on [t i, t (i+1)), each g i Lipschitz on the closed piece.

theorem Zeta5Irrational.psum_mono {f g : ℝ → ℝ} {a b K : ℝ} (ha : 0 < a) (hab : a ≤ b) (hK : 0 < K) (h : ∀ x ∈ Set.Ico a b, f x ≤ g x) : psum f a b K ≤ psum g a b K

theorem Zeta5Irrational.psum_piecewise_le' {f : ℝ → ℝ} {g : ℕ → ℝ → ℝ} {t : ℕ → ℝ} {L : ℝ} (m : ℕ) (ht0 : 0 < t 0) (hmono : ∀ i < m, t i < t (i + 1)) (hL : 0 ≤ L) (hcont : ∀ i < m, ContinuousOn (g i) (Set.Icc (t i) (t (i + 1)))) (hLip : ∀ i < m, ∀ x ∈ Set.Icc (t i) (t (i + 1)), ∀ y ∈ Set.Icc (t i) (t (i + 1)), |g i x - g i y| ≤ L * |x - y|) (hfg : ∀ i < m, ∀ x ∈ Set.Ico (t i) (t (i + 1)), f x ≤ g i x) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (K : ℝ) in Filter.atTop, psum f (t 0) (t m) K / K ^ 2 ≤ (∑ i ∈ Finset.range m, ∫ (x : ℝ) in t i..t (i + 1), g i x / x ^ 3) + ε

The piecewise version with f ≤ g i on the pieces.