uniformRingSample

formal source

  58
  59/-- A uniform charged ring sample: every increment on the ring carries the
  60same phase step, so the total winding is exactly `m`. -/
  61noncomputable def uniformRingSample (n : ℕ) (m : ℤ) : AnnularRingSample (n + 1) where
  62  increments := fun _ => -(2 * Real.pi * m) / (8 * (n + 1) : ℝ)
  63  winding := m
  64  winding_constraint := by
  65    simp [Finset.sum_const, nsmul_eq_mul]
  66    field_simp
  67
  68/-- A mesh whose every ring has the same winding charge `m`. -/
  69noncomputable def uniformChargeMesh (N : ℕ) (m : ℤ) : AnnularMesh N where
  70  rings := fun n => uniformRingSample n.val m
  71  charge := m
  72  uniform_charge := by
  73    intro n
  74    rfl
  75
  76/-- The Fredholm–Carleman carrier associated with the Euler product.
  77    C(s) = det₂(I−A(s))² = ∏_p (1−p^{−s})² exp(2p^{−s}).
  78    Holomorphic and nonvanishing on Re(s) > 1/2. -/
  79structure EulerCarrier where
  80  /-- The half-plane where the carrier is regular. -/
  81  halfPlane : ℝ
  82  halfPlane_gt : 1/2 < halfPlane
  83  /-- Logarithmic derivative bound on compact subsets. -/
  84  logDerivBound : ℝ → ℝ
  85  /-- Since the bound is real-valued, finiteness is automatic. -/
  86  logDerivBound_finite : ∀ σ, halfPlane < σ → True
  87  /-- The carrier is nonvanishing. -/
  88  nonvanishing : Prop
  89
  90/-- The standard Euler carrier for the Riemann zeta function.
  91    logDerivBound(σ) = 2∑_p (log p)p^{−2σ}/(1−p^{−σ}). -/