norm_eulerPrimePowerComplex_lt_one

formal source

 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
 433  simpa using h
 434
 435/-- The per-prime Euler eigenvalue stays strictly inside the unit disk on any
 436sensor circle contained in the strip. This is the first directly usable strip
 437estimate for building a sampled perturbation witness. -/
 438theorem norm_eulerPrimePowerComplex_lt_one_on_sensorCircle
 439    (sensor : DefectSensor) {r θ : ℝ}
 440    (hr_nonneg : 0 ≤ r) (hr : r < sensor.realPart - 1 / 2)
 441    (p : Nat.Primes) :
 442    ‖eulerPrimePowerComplex p (defectSensorCirclePoint sensor r θ)‖ < 1 := by
 443  have hs : 0 < (defectSensorCirclePoint sensor r θ).re := by
 444    have hstrip := defectSensorCirclePoint_mem_strip (sensor := sensor) (θ := θ) hr_nonneg hr
 445    linarith
 446  exact norm_eulerPrimePowerComplex_lt_one hs p
 447
 448/-- Therefore the factor `(1 - p^{-s})` never vanishes on the open right
 449half-plane. -/
 450theorem one_sub_eulerPrimePowerComplex_ne_zero {s : ℂ} (hs : 0 < s.re)
 451    (p : Nat.Primes) :
 452    1 - eulerPrimePowerComplex p s ≠ 0 := by