realizedDefectAnnularExcessBounded_of_ringRegularErrorBound

formal source

 239
 240/-- A uniform ring-level regular-part error bound implies bounded annular
 241excess for the realized family. -/
 242theorem realizedDefectAnnularExcessBounded_of_ringRegularErrorBound
 243    (fam : DefectSampledFamily) (hreg : RingRegularErrorBound fam) :
 244    RealizedDefectAnnularExcessBounded fam := by
 245  obtain ⟨K, hK⟩ := hreg.total_error_bounded
 246  refine ⟨K, ?_⟩
 247  intro N
 248  exact le_trans
 249    (annularExcess_le_sum_of_ringCost_le_topologicalFloor_plus_regularError fam hreg N)
 250    (hK N)
 251
 252/-- A uniform total-cost bound immediately gives a uniform excess bound, since
 253the topological floor is nonnegative. -/
 254theorem realizedDefectAnnularExcessBounded_of_costBounded
 255    (fam : DefectSampledFamily)
 256    (hcost : RealizedDefectAnnularCostBounded fam) :
 257    RealizedDefectAnnularExcessBounded fam := by
 258  obtain ⟨K, hK⟩ := hcost
 259  refine ⟨K, ?_⟩
 260  intro N
 261  unfold annularExcess
 262  have hfloor : 0 ≤ annularTopologicalFloor N (fam.sensor.charge) :=
 263    annularTopologicalFloor_nonneg N fam.sensor.charge
 264  have hcostN : annularCost (fam.mesh N) ≤ K := hK N
 265  rw [fam.charge_spec N]
 266  linarith
 267
 268/-- If the sensor charge is zero, then bounded excess is equivalent to bounded
 269total cost because the topological floor vanishes identically. -/
 270theorem realizedDefectCostBounded_of_charge_zero_and_excessBounded
 271    (fam : DefectSampledFamily)
 272    (hzero : fam.sensor.charge = 0)