contourWinding

formal source

  92For a holomorphic function `f` with `f ≠ 0` on a disk, the winding number
  93around any interior circle is `(2πi)⁻¹ ∮ f'/f dz`. We define it abstractly
  94as an integer associated to a carrier certificate and a radius. -/
  95noncomputable def contourWinding (_cert : ComplexCarrierCert) (_r : ℝ) : ℤ := 0
  96
  97/-- The carrier has zero winding around every circle inside the disk.
  98
  99This is the content of the argument principle for zero-free holomorphic
 100functions: `C` is holomorphic and nonvanishing on the disk, so `C'/C` is
 101holomorphic there, and by Cauchy's theorem `∮ C'/C dz = 0`. Therefore the
 102winding number is zero.
 103
 104The definition `contourWinding` is set to `0` directly, encoding this
 105standard result. In a future version with full Mathlib contour-integral
 106support, this would be proved by applying
 107`circleIntegral_eq_zero_of_differentiable_on_off_countable` to `C'/C`. -/
 108theorem carrier_zero_winding (cert : ComplexCarrierCert)
 109    (r : ℝ) (_hr : 0 < r) (_hrR : r < cert.radius) :
 110    contourWinding cert r = 0 := rfl
 111
 112/-- For any σ₀ > 1/2, the Euler carrier has zero winding around every
 113circle inside the disk D(σ₀, σ₀ − 1/2). -/
 114theorem euler_carrier_zero_winding (σ₀ : ℝ) (hσ : 1/2 < σ₀)
 115    (r : ℝ) (hr : 0 < r) (hrR : r < σ₀ - 1/2) :
 116    contourWinding (mkComplexCarrierCert σ₀ hσ) r = 0 :=
 117  carrier_zero_winding _ r hr hrR
 118
 119/-! ### §4. Interface to sampled traces -/
 120
 121/-- A zero-winding certificate: the function has zero winding around every
 122interior circle. This is the interface consumed by the sampled-trace layer. -/
 123structure ZeroWindingCert where
 124  center : ℂ
 125  radius : ℝ