realizedDefectAnnularExcessBounded_of_costBounded

formal source

 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)
 273    (hexcess : RealizedDefectAnnularExcessBounded fam) :
 274    RealizedDefectAnnularCostBounded fam := by
 275  obtain ⟨K, hK⟩ := hexcess
 276  refine ⟨K, ?_⟩
 277  intro N
 278  have hfloor : annularTopologicalFloor N (fam.sensor.charge) = 0 := by
 279    rw [hzero, annularTopologicalFloor_zero]
 280  have hexN : annularExcess (fam.mesh N) ≤ K := hK N
 281  unfold annularExcess at hexN
 282  rw [fam.charge_spec N, hfloor] at hexN
 283  simpa using hexN
 284