defectAnnularMesh_charge

formal source

  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
  71
  72/-- Choose one phase family attached to a hypothetical defect sensor.
  73
  74This uses the strengthened existential package
  75`defect_phase_family_with_perturbation_exists`, so the chosen family comes with
  76the perturbation witness needed downstream for the annular excess argument. -/
  77noncomputable def chosenDefectPhaseFamily (sensor : DefectSensor)
  78    (hm : sensor.charge ≠ 0) : DefectPhaseFamily :=
  79  Classical.choose (defect_phase_family_with_perturbation_exists sensor hm)