canonicalDefectSampledFamily

formal source

  93    (defect_phase_family_with_perturbation_exists sensor hm)).2)
  94
  95/-- The canonical realized sampled family attached to a hypothetical defect. -/
  96noncomputable def canonicalDefectSampledFamily (sensor : DefectSensor)
  97    (hm : sensor.charge ≠ 0) : DefectSampledFamily :=
  98  (chosenDefectPhaseFamily sensor hm).toSampledFamily
  99
 100/-- The canonical sampled family remembers the requested sensor. -/
 101theorem canonicalDefectSampledFamily_sensor (sensor : DefectSensor)
 102    (hm : sensor.charge ≠ 0) :
 103    (canonicalDefectSampledFamily sensor hm).sensor = sensor :=
 104  chosenDefectPhaseFamily_sensor sensor hm
 105
 106/-- Every mesh in the canonical sampled family has the requested sensor charge. -/
 107theorem canonicalDefectSampledFamily_charge (sensor : DefectSensor)
 108    (hm : sensor.charge ≠ 0) (N : ℕ) :
 109    ((canonicalDefectSampledFamily sensor hm).mesh N).charge = sensor.charge := by
 110  simpa [canonicalDefectSampledFamily_sensor sensor hm] using
 111    ((canonicalDefectSampledFamily sensor hm).charge_spec N)
 112
 113/-! ### §3. Refined bounded-cost proposition -/
 114
 115/-- The annular cost of a realized sampled family is bounded independently of
 116mesh refinement. This is the realizable replacement for the previous
 117over-strong quantification over arbitrary `AnnularMesh` values. -/
 118def RealizedDefectAnnularCostBounded (fam : DefectSampledFamily) : Prop :=
 119  ∃ K : ℝ, ∀ N : ℕ, annularCost (fam.mesh N) ≤ K
 120
 121/-- The annular excess of a realized sampled family is bounded independently of
 122mesh refinement. This is the quantitatively plausible part of the defect-cost
 123story: after removing the topological floor, only the regular remainder should
 124need analytic control. -/
 125def RealizedDefectAnnularExcessBounded (fam : DefectSampledFamily) : Prop :=
 126  ∃ K : ℝ, ∀ N : ℕ, annularExcess (fam.mesh N) ≤ K