theorem
proved
tactic proof
norm_eulerPrimeLogDerivTermComplex_le
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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)`. -/