theorem
proved
tactic proof
norm_eulerPrimePowerComplex
show as:
view Lean formalization →
formal statement (Lean)
402theorem norm_eulerPrimePowerComplex (p : Nat.Primes) (s : ℂ) :
403 ‖eulerPrimePowerComplex p s‖ = Real.exp (-s.re * primeLog p) := by
proof body
Tactic-mode proof.
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. -/