carrierDerivBound_summable

proof body

Tactic-mode proof.

 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
 272    exact le_of_lt (Real.log_pos hp_one)
 273  have h1 :
 274      (p : ℝ) ^ (-2 * σ₀) * Real.log p ≤
 275        (p : ℝ) ^ (-2 * σ₀) * ((p : ℝ) ^ ε / ε) := by
 276    exact mul_le_mul_of_nonneg_left hlog_le ha_nonneg
 277  calc
 278    carrierDerivTerm p σ₀
 279        = (p : ℝ) ^ (-2 * σ₀) * Real.log p * (1 - (p : ℝ) ^ (-σ₀))⁻¹ := by
 280            rw [carrierDerivTerm, div_eq_mul_inv]
 281    _ ≤ ((p : ℝ) ^ (-2 * σ₀) * Real.log p) * (1 - (2 : ℝ) ^ (-σ₀))⁻¹ := by
 282          gcongr
 283    _ ≤ ((p : ℝ) ^ (-2 * σ₀) * ((p : ℝ) ^ ε / ε)) * (1 - (2 : ℝ) ^ (-σ₀))⁻¹ := by
 284          gcongr
 285    _ = K * (p : ℝ) ^ (-(σ₀ + 1 / 2)) := by
 286          have hpow :
 287              (p : ℝ) ^ (-2 * σ₀) * (p : ℝ) ^ ε =
 288                (p : ℝ) ^ (-(σ₀ + 1 / 2)) := by
 289            rw [← Real.rpow_add (by positivity)]
 290            unfold ε
 291            congr 1
 292            ring
 293          unfold K
 294          rw [div_eq_mul_inv, mul_assoc, ← hpow]
 295          ring
 296
 297/-- The carrier logarithmic derivative bound is finite for σ₀ > 1/2. -/