mkSampledRing

formal source

  76Uses uniform increments (all zero) since the carrier has zero winding.
  77The actual phase values are zero because the net phase change around
  78any circle is zero for a zero-winding function. -/
  79def mkSampledRing (cert : ZeroWindingCert) (n : ℕ) (_hn : 0 < n)
  80    (r : ℝ) (hr : 0 < r) (_hrR : r < cert.radius) :
  81    SampledRing n where
  82  center := cert.center
  83  radius := r
  84  radius_pos := hr
  85  increments := fun _ => 0
  86  winding := 0
  87  winding_constraint := by simp
  88  winding_from_contour := rfl
  89
  90/-! ### §3. Sampled mesh -/
  91
  92/-- A sampled mesh: N concentric sampled rings with uniform charge 0. -/
  93structure SampledMesh (N : ℕ) where
  94  rings : (n : Fin N) → SampledRing (n.val + 1)
  95  charge_zero : ∀ n, (rings n).winding = 0
  96
  97/-- Convert a `SampledMesh` to an `AnnularMesh` with charge 0. -/
  98def SampledMesh.toAnnularMesh {N : ℕ} (sm : SampledMesh N) :
  99    AnnularMesh N where
 100  rings := fun n => (sm.rings n).toAnnularRingSample
 101  charge := 0
 102  uniform_charge := fun n => by
 103    simp [SampledRing.toAnnularRingSample]
 104    exact sm.charge_zero n
 105
 106/-- The converted mesh has charge 0. -/
 107theorem SampledMesh.toAnnularMesh_charge_zero {N : ℕ} (sm : SampledMesh N) :
 108    sm.toAnnularMesh.charge = 0 := rfl
 109