def
definition
def or abbrev
ringRegularErrorBound_of_ringPerturbationControl
show as:
view Lean formalization →
formal statement (Lean)
181noncomputable def ringRegularErrorBound_of_ringPerturbationControl
182 (fam : DefectSampledFamily) (hctrl : RingPerturbationControl fam) :
183 RingRegularErrorBound fam := by
proof body
Definition body.
184 refine
185 { error := realizedRingPerturbationError fam
186 ring_estimate := ?_
187 total_error_bounded := hctrl.total_bounded }
188 intro N n
189 have hcharge : ((fam.mesh N).rings n).winding = (fam.mesh N).charge := by
190 rw [((fam.mesh N).uniform_charge n)]
191 have hsmall_ring :
192 ∀ j : Fin (8 * n.val.succ),
193 |Real.log Constants.phi *
194 (((fam.mesh N).rings n).increments j -
195 (-(2 * Real.pi * ((((fam.mesh N).rings n).winding : ℤ) : ℝ)) /
196 (8 * n.val.succ : ℝ)))| ≤ 1 := by
197 intro j
198 have hj := hctrl.small N n j
199 simpa [hcharge, Nat.succ_eq_add_one] using hj
200 have hring :=
201 ringCost_le_topologicalFloor_add_linear_quadratic_error
202 (Nat.succ_pos n.val) ((fam.mesh N).rings n) hsmall_ring
203 rw [hcharge] at hring
204 simpa [realizedRingPerturbationError, add_assoc] using hring
205
206/-- Summing the ring-level estimate yields a bound for annular excess.
207
208This is the unconditional algebraic step:
209
210`ringCost ≤ topologicalFloor + regularError`
211
212on each ring implies
213
214`annularExcess ≤ ∑ regularError`
215
216on the full annulus. -/