carrierDerivBound_summable

formal source

 238/-- The derivative bound series converges for σ₀ > 1/2.
 239    Dominated by C·∑_p p^{−2σ₀}·log p, which converges since
 240    log p ≤ p^ε for any ε > 0, and 2σ₀ − ε > 1 for small ε. -/
 241theorem carrierDerivBound_summable {σ₀ : ℝ} (hσ : 1/2 < σ₀) :
 242    Summable (fun (p : Nat.Primes) => carrierDerivTerm p σ₀) := by
 243  let ε : ℝ := σ₀ - 1 / 2
 244  let K : ℝ := (1 / ε) * (1 / (1 - (2 : ℝ) ^ (-σ₀)))
 245  have hε_pos : 0 < ε := by
 246    unfold ε
 247    linarith
 248  have hKsum : Summable (fun p : Nat.Primes => K * (p : ℝ) ^ (-(σ₀ + 1 / 2))) := by
 249    exact ((Nat.Primes.summable_rpow).2 (by linarith : -(σ₀ + 1 / 2 : ℝ) < -1)).mul_left K
 250  refine hKsum.of_nonneg_of_le (fun p => carrierDerivTerm_nonneg hσ p) ?_
 251  intro p
 252  have hp_one : (1 : ℝ) < p := by exact_mod_cast p.prop.one_lt
 253  have hp_nonneg : 0 ≤ (p : ℝ) := by positivity
 254  have hlog_le : Real.log p ≤ (p : ℝ) ^ ε / ε := by
 255    simpa [ε, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using
 256      (Real.log_le_rpow_div hp_nonneg hε_pos)
 257  have hpow_ge : (2 : ℝ) ^ σ₀ ≤ (p : ℝ) ^ σ₀ := by
 258    exact Real.rpow_le_rpow (by norm_num) (by exact_mod_cast p.prop.two_le) (le_of_lt (by linarith))
 259  have hpow_ge_pos : 0 < (2 : ℝ) ^ σ₀ := Real.rpow_pos_of_pos (by norm_num) _
 260  have hx_le : (p : ℝ) ^ (-σ₀) ≤ (2 : ℝ) ^ (-σ₀) := by
 261    rw [Real.rpow_neg (by positivity), Real.rpow_neg (by positivity)]
 262    simpa [one_div] using one_div_le_one_div_of_le hpow_ge_pos hpow_ge
 263  have hden_pos : 0 < 1 - (2 : ℝ) ^ (-σ₀) := by
 264    have hlt : (2 : ℝ) ^ (-σ₀) < 1 := Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)
 265    linarith
 266  have hden_le : 1 - (2 : ℝ) ^ (-σ₀) ≤ 1 - (p : ℝ) ^ (-σ₀) := by
 267    linarith
 268  have hrecip_le : (1 - (p : ℝ) ^ (-σ₀))⁻¹ ≤ (1 - (2 : ℝ) ^ (-σ₀))⁻¹ := by
 269    simpa [one_div] using one_div_le_one_div_of_le hden_pos hden_le
 270  have ha_nonneg : 0 ≤ (p : ℝ) ^ (-2 * σ₀) := by positivity
 271  have hlog_nonneg : 0 ≤ Real.log p := by