meromorphic_phase_charge

formal source

 107
 108/-! ### §2. Phase charge equals negative order -/
 109
 110theorem meromorphic_phase_charge (w : LocalMeromorphicWitness)
 111    (r : ℝ) (hr : 0 < r) (_hrw : r < w.radius) :
 112    ∃ cpd : ContinuousPhaseData,
 113      cpd.center = w.center ∧ cpd.radius = r ∧ cpd.charge = -w.order := by
 114  simpa using zpow_phase_charge w.center r hr w.order
 115
 116/-! ### §3. Defect sensor phase families -/
 117
 118structure DefectPhaseFamily where
 119  sensor : DefectSensor
 120  witnessRadius : ℝ
 121  witnessRadius_pos : 0 < witnessRadius
 122  phaseAtLevel : (n : ℕ) → 0 < n → ContinuousPhaseData
 123  charge_uniform : ∀ n hn, (phaseAtLevel n hn).charge = sensor.charge
 124
 125/-- A constant-radius phase package carrying the prescribed defect charge. -/
 126noncomputable def pureDefectPhaseData (sensor : DefectSensor) :
 127    (n : ℕ) → 0 < n → ContinuousPhaseData :=
 128  fun n hn =>
 129    { center := (sensor.realPart : ℂ)
 130      radius := 1
 131      radius_pos := by norm_num
 132      phase := fun θ => (-(sensor.charge : ℤ) : ℝ) * θ
 133      phase_continuous := by
 134        continuity
 135      charge := sensor.charge
 136      phase_winding := by
 137        simp [sub_eq_add_neg]
 138        ring }
 139
 140/-- A defect phase family with the correct charge but no regular perturbation. -/