norm_eulerPrimePowerComplex

formal source

 399
 400/-- Norm of the complex Euler eigenvalue is controlled exactly by the real part
 401of `s`. -/
 402theorem norm_eulerPrimePowerComplex (p : Nat.Primes) (s : ℂ) :
 403    ‖eulerPrimePowerComplex p s‖ = Real.exp (-s.re * primeLog p) := by
 404  have hp_nonneg : 0 ≤ (p : ℝ) := by positivity
 405  have hlog :
 406      ((primeLog p : ℝ) : ℂ) = Complex.log (p : ℂ) := by
 407    simpa [primeLog] using (Complex.ofReal_log hp_nonneg).symm
 408  calc
 409    ‖eulerPrimePowerComplex p s‖
 410        = ‖Complex.exp (-(s * Complex.log (p : ℂ)))‖ := by
 411            simp [eulerPrimePowerComplex, hlog]
 412    _ = Real.exp ((-(s * Complex.log (p : ℂ))).re) := by
 413          simpa using Complex.norm_exp (-(s * Complex.log (p : ℂ)))
 414    _ = Real.exp (-s.re * primeLog p) := by
 415          congr 1
 416          rw [← hlog]
 417          simp [Complex.mul_re]
 418
 419/-- On the open right half-plane, each Euler eigenvalue has norm strictly less
 420than `1`. This is the basic denominator-separation fact needed for all later
 421prime-level perturbation estimates. -/
 422theorem norm_eulerPrimePowerComplex_lt_one {s : ℂ} (hs : 0 < s.re)
 423    (p : Nat.Primes) :
 424    ‖eulerPrimePowerComplex p s‖ < 1 := by
 425  rw [norm_eulerPrimePowerComplex]
 426  have hlog_pos : 0 < primeLog p := by
 427    have hp_one : (1 : ℝ) < p := by
 428      exact_mod_cast p.prop.one_lt
 429    simpa [primeLog] using Real.log_pos hp_one
 430  have hexp_lt : -s.re * primeLog p < 0 := by
 431    nlinarith
 432  have h := Real.exp_lt_exp.mpr hexp_lt