138structure RingRegularErrorBound (fam : DefectSampledFamily) where 139 error : ∀ N : ℕ, Fin N → ℝ 140 ring_estimate : ∀ N : ℕ, ∀ n : Fin N, 141 ringCost ((fam.mesh N).rings n) ≤ 142 topologicalFloor (n.val + 1) ((fam.mesh N).charge) + error N n 143 total_error_bounded : ∃ K : ℝ, ∀ N : ℕ, ∑ n : Fin N, error N n ≤ K 144 145/-- The explicit linear-plus-quadratic perturbation error on one realized ring. 146 147This is the error term delivered by 148`ringCost_le_topologicalFloor_add_linear_quadratic_error` once the ring 149increments are written as the pure winding increment plus a regular 150perturbation. -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.