norm_eulerPrimeLogDerivTermComplex_le

formal source

 487/-- Norm bound for the per-prime complex log-derivative contribution.
 488The numerator uses `norm_mul`/`norm_pow`/`norm_ofReal`, and the denominator
 489uses the reverse triangle inequality `1 − ‖z‖ ≤ ‖1 − z‖`. -/
 490theorem norm_eulerPrimeLogDerivTermComplex_le {s : ℂ} (hs : 0 < s.re)
 491    (p : Nat.Primes) :
 492    ‖eulerPrimeLogDerivTermComplex p s‖ ≤
 493      primeLog p * ‖eulerPrimePowerComplex p s‖ ^ 2 /
 494        (1 - ‖eulerPrimePowerComplex p s‖) := by
 495  have hz_lt := norm_eulerPrimePowerComplex_lt_one hs p
 496  have hlog_nonneg : 0 ≤ primeLog p :=
 497    le_of_lt (by simpa [primeLog] using Real.log_pos (by exact_mod_cast p.prop.one_lt))
 498  have hden_pos : 0 < 1 - ‖eulerPrimePowerComplex p s‖ := by linarith
 499  have hden_le : 1 - ‖eulerPrimePowerComplex p s‖ ≤ ‖1 - eulerPrimePowerComplex p s‖ := by
 500    calc 1 - ‖eulerPrimePowerComplex p s‖
 501        = ‖(1 : ℂ)‖ - ‖eulerPrimePowerComplex p s‖ := by rw [norm_one]
 502      _ ≤ ‖(1 : ℂ) - eulerPrimePowerComplex p s‖ := norm_sub_norm_le _ _
 503  have hlog_norm : ‖(↑(primeLog p) : ℂ)‖ = primeLog p := by
 504    rw [Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg hlog_nonneg]
 505  unfold eulerPrimeLogDerivTermComplex
 506  rw [norm_div, norm_mul, norm_pow, hlog_norm]
 507  exact div_le_div_of_nonneg_left (mul_nonneg hlog_nonneg (sq_nonneg _)) hden_pos hden_le
 508
 509/-- The norm-form bound equals the real carrier derivative term at `σ = Re(s)`. -/
 510theorem norm_form_eq_carrierDerivTerm (p : Nat.Primes) (s : ℂ) :
 511    primeLog p * ‖eulerPrimePowerComplex p s‖ ^ 2 /
 512      (1 - ‖eulerPrimePowerComplex p s‖) = carrierDerivTerm p s.re := by
 513  have hp_pos : (0 : ℝ) < p := by exact_mod_cast p.prop.pos
 514  rw [norm_eulerPrimePowerComplex_eq_rpow]
 515  unfold carrierDerivTerm primeLog
 516  have hsq : ((p : ℝ) ^ (-s.re)) ^ 2 = (p : ℝ) ^ (-2 * s.re) := by
 517    rw [sq, ← Real.rpow_add hp_pos]; congr 1; ring
 518  rw [hsq, mul_comm (Real.log (p : ℝ)) _]
 519
 520/-- The per-prime complex log-derivative term is dominated by the real carrier