defectAnnularMesh

formal source

  37
  38/-- Build an `AnnularMesh` from a `DefectPhaseFamily` by sampling each ring at
  39the canonical `8n` equispaced angles. -/
  40def defectAnnularMesh (dpf : DefectPhaseFamily) (N : ℕ) : AnnularMesh N where
  41  rings := fun k =>
  42    (dpf.phaseAtLevel (k.val + 1) (Nat.succ_pos k.val)).toAnnularRingSample
  43      (k.val + 1) (Nat.succ_pos k.val)
  44  charge := dpf.sensor.charge
  45  uniform_charge := fun k =>
  46    dpf.charge_uniform (k.val + 1) (Nat.succ_pos k.val)
  47
  48/-- The mesh obtained from phase sampling has the correct total charge. -/
  49theorem defectAnnularMesh_charge (dpf : DefectPhaseFamily) (N : ℕ) :
  50    (defectAnnularMesh dpf N).charge = dpf.sensor.charge :=
  51  rfl
  52
  53/-! ### §2. Realized sampled families -/
  54
  55/-- A realized sampled family of annular meshes attached to one defect sensor.
  56
  57Unlike a bare `AnnularTrace`, this object is intended to arise from the actual
  58phase-sampling construction for `ζ⁻¹`, not from an arbitrary synthetic mesh
  59family. -/
  60structure DefectSampledFamily where
  61  sensor : DefectSensor
  62  mesh : ∀ N : ℕ, AnnularMesh N
  63  charge_spec : ∀ N : ℕ, (mesh N).charge = sensor.charge
  64
  65/-- Convert a `DefectPhaseFamily` to its realized sampled annular family. -/
  66def DefectPhaseFamily.toSampledFamily (dpf : DefectPhaseFamily) :
  67    DefectSampledFamily where
  68  sensor := dpf.sensor
  69  mesh := defectAnnularMesh dpf
  70  charge_spec := defectAnnularMesh_charge dpf