winding_additive

formal source

  89
  90Since C is holomorphic and nonvanishing, `wind(C) = 0`, hence
  91`wind(C⁻¹) = -wind(C) = 0`, and `wind(ζ⁻¹) = wind(C/ζ)`. -/
  92theorem winding_additive (w₁ w₂ : WindingData) (hw : w₁.center = w₂.center)
  93    (hr : w₁.radius = w₂.radius) :
  94    ∃ w : WindingData, w.charge = w₁.charge + w₂.charge ∧
  95      w.center = w₁.center ∧ w.radius = w₁.radius :=
  96  ⟨{ center := w₁.center, radius := w₁.radius, radius_pos := w₁.radius_pos,
  97     charge := w₁.charge + w₂.charge }, rfl, rfl, rfl⟩
  98
  99/-- The winding of a reciprocal negates the charge. -/
 100theorem winding_reciprocal (w : WindingData) :
 101    ∃ w' : WindingData, w'.charge = -w.charge ∧
 102      w'.center = w.center ∧ w'.radius = w.radius :=
 103  ⟨{ w with charge := -w.charge }, rfl, rfl, rfl⟩
 104
 105/-! ### §4. Defect winding equals sensor charge -/
 106
 107/-- A defect sensor at ρ with charge m creates winding data with charge m.
 108
 109This is the content of the argument principle: if ζ has a zero of
 110multiplicity m at ρ, then ζ⁻¹ has a pole of order m, and the winding
 111number of ζ⁻¹ around ρ is −m (or equivalently, the winding of ζ is m).
 112
 113In the RS framework, the defect sensor records this charge directly. -/
 114def defectWindingData (sensor : DefectSensor) (r : ℝ) (hr : 0 < r) :
 115    WindingData where
 116  center := ⟨sensor.realPart, 0⟩
 117  radius := r
 118  radius_pos := hr
 119  charge := sensor.charge
 120
 121/-- The defect winding charge equals the sensor charge. -/
 122theorem defect_winding_eq_charge (sensor : DefectSensor) (r : ℝ) (hr : 0 < r) :