defectSensorCirclePoint_mem_strip

formal source

 389
 390/-- Any circle around the sensor center whose radius stays inside the strip still
 391lies in the open half-plane `Re(s) > 1/2`. -/
 392theorem defectSensorCirclePoint_mem_strip
 393    (sensor : DefectSensor) {r θ : ℝ}
 394    (hr_nonneg : 0 ≤ r) (hr : r < sensor.realPart - 1 / 2) :
 395    1 / 2 < (defectSensorCirclePoint sensor r θ).re := by
 396  rw [defectSensorCirclePoint_re]
 397  have hcos : -1 ≤ Real.cos θ := Real.neg_one_le_cos θ
 398  nlinarith
 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)