RingPerturbationControl

formal source

 168The `total_bounded` field says the resulting linear-plus-quadratic error sums
 169are uniformly bounded across refinement depth `N`. This is exactly the remaining
 170analytic input needed after the perturbative `phiCost` reduction. -/
 171structure RingPerturbationControl (fam : DefectSampledFamily) where
 172  small : ∀ N : ℕ, ∀ n : Fin N, ∀ j : Fin (8 * (n.val + 1)),
 173    |Real.log Constants.phi *
 174        (((fam.mesh N).rings n).increments j -
 175          (-(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)))| ≤ 1
 176  total_bounded : ∃ K : ℝ, ∀ N : ℕ,
 177    ∑ n : Fin N, realizedRingPerturbationError fam N n ≤ K
 178
 179/-- A perturbation-control package yields the ring-regular-error package needed
 180for bounded annular excess. -/
 181noncomputable def ringRegularErrorBound_of_ringPerturbationControl
 182    (fam : DefectSampledFamily) (hctrl : RingPerturbationControl fam) :
 183    RingRegularErrorBound fam := by
 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