uniformChargeMesh

formal source

  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^{−σ}). -/
  92noncomputable def zetaCarrier : EulerCarrier where
  93  halfPlane := 1
  94  halfPlane_gt := by norm_num
  95  logDerivBound σ := 2 * σ
  96  logDerivBound_finite σ _ := by trivial
  97  nonvanishing := True
  98
  99/-! ### §2. Defect sensor -/