SampledMesh

formal source

  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
 110/-! ### §4. Constructing sampled meshes from a zero-winding cert -/
 111
 112/-- Construct a full sampled mesh from a `ZeroWindingCert`.
 113Uses a fixed radius `R/2` for all rings (inside the disk). -/
 114noncomputable def mkSampledMesh (cert : ZeroWindingCert) (N : ℕ) :
 115    SampledMesh N where
 116  rings := fun n =>
 117    mkSampledRing cert (n.val + 1) (Nat.succ_pos _)
 118      (cert.radius / 2)
 119      (by linarith [cert.radius_pos])
 120      (by linarith [cert.radius_pos])
 121  charge_zero := fun _ => rfl
 122
 123/-- The sampled mesh from a cert has charge 0. -/