defectSensorCirclePoint_re

formal source

 382  zetaReciprocal (defectSensorCirclePoint sensor r θ)
 383
 384/-- Explicit real-part formula for the current sensor-circle parameterization. -/
 385theorem defectSensorCirclePoint_re (sensor : DefectSensor) (r θ : ℝ) :
 386    (defectSensorCirclePoint sensor r θ).re = sensor.realPart + r * Real.cos θ := by
 387  rw [defectSensorCirclePoint, defectSensorCenter, circleMap]
 388  simp [Complex.mul_re, Complex.exp_ofReal_mul_I_re]
 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