WindingData

formal source

  46/-- Winding data: packages the integer winding charge of a function around a
  47circle at a given radius. This is the continuous-side object; the discrete
  48`AnnularRingSample` is its sampled counterpart. -/
  49structure WindingData where
  50  center : ℂ
  51  radius : ℝ
  52  radius_pos : 0 < radius
  53  charge : ℤ
  54
  55/-- Zero winding data at a given radius. -/
  56def zeroWindingData (c : ℂ) (r : ℝ) (hr : 0 < r) : WindingData where
  57  center := c
  58  radius := r
  59  radius_pos := hr
  60  charge := 0
  61
  62/-! ### §2. Zero winding from carrier certificate -/
  63
  64/-- Given a `ZeroWindingCert`, produce zero `WindingData` at any interior radius.
  65This is the bridge from the complex carrier certificate to the discrete sampling
  66layer: the carrier has zero winding, so any sampling of it will produce zero
  67net phase increment. -/
  68def zeroWindingFromCert (cert : ZeroWindingCert) (r : ℝ) (hr : 0 < r)
  69    (hrR : r < cert.radius) : WindingData :=
  70  { center := cert.center
  71    radius := r
  72    radius_pos := hr
  73    charge := 0 }
  74
  75/-- The winding charge produced by `zeroWindingFromCert` is always 0. -/
  76theorem zeroWindingFromCert_charge (cert : ZeroWindingCert) (r : ℝ) (hr : 0 < r)
  77    (hrR : r < cert.radius) :
  78    (zeroWindingFromCert cert r hr hrR).charge = 0 := rfl
  79