canonicalDefectSampledFamily_excess_bounded

formal source

 435  exact ringRegularErrorBound_of_ringPerturbationControl _
 436    (canonicalDefectSampledFamily_ringPerturbationControl sensor hm)
 437
 438theorem canonicalDefectSampledFamily_excess_bounded (sensor : DefectSensor)
 439    (hm : sensor.charge ≠ 0) :
 440    RealizedDefectAnnularExcessBounded
 441      (canonicalDefectSampledFamily sensor hm) := by
 442  exact realizedDefectAnnularExcessBounded_of_ringRegularErrorBound _
 443    (canonicalDefectSampledFamily_ringRegularErrorBound sensor hm)
 444
 445/-- Nonzero charge forces the realized sampled family cost to exceed any bound.
 446
 447This is just `defect_cost_unbounded` specialized to the meshes of one realized
 448family. The theorem is completely unconditional. -/
 449theorem defectSampledFamily_unbounded (fam : DefectSampledFamily)
 450    (hm : fam.sensor.charge ≠ 0) :
 451    ∀ B : ℝ, ∃ N : ℕ, B < annularCost (fam.mesh N) := by
 452  intro B
 453  obtain ⟨N, hN⟩ := defect_cost_unbounded fam.sensor hm B
 454  refine ⟨N, ?_⟩
 455  have hcharge : ∀ n, ((fam.mesh N).rings n).winding = fam.sensor.charge := by
 456    intro n
 457    rw [((fam.mesh N).uniform_charge n), fam.charge_spec N]
 458  exact hN (fam.mesh N) hcharge
 459
 460/-- A realized sampled family with nonzero charge can never have bounded annular
 461cost. This is the contradiction theorem underlying the refined Axiom 2. -/
 462theorem not_realizedDefectAnnularCostBounded (fam : DefectSampledFamily)
 463    (hm : fam.sensor.charge ≠ 0) :
 464    ¬ RealizedDefectAnnularCostBounded fam := by
 465  intro hbound
 466  obtain ⟨K, hK⟩ := hbound
 467  obtain ⟨N, hN⟩ := defectSampledFamily_unbounded fam hm K
 468  exact not_lt_of_ge (hK N) hN