defectSensorCirclePoint

formal source

 373/-- Sample a point on a circle around the current sensor center. This is the
 374geometric entry point for replacing abstract phase families by actual samples of
 375`ζ⁻¹` or Euler factors on circles. -/
 376noncomputable def defectSensorCirclePoint (sensor : DefectSensor) (r θ : ℝ) : ℂ :=
 377  circleMap (defectSensorCenter sensor) r θ
 378
 379/-- The reciprocal zeta function sampled on a sensor circle. -/
 380noncomputable def zetaReciprocalOnSensorCircle
 381    (sensor : DefectSensor) (r θ : ℝ) : ℂ :=
 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