pith. machine review for the scientific record. sign in
def definition def or abbrev

realizedRingPerturbationError

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 151noncomputable def realizedRingPerturbationError (fam : DefectSampledFamily)
 152    (N : ℕ) (n : Fin N) : ℝ :=

proof body

Definition body.

 153  let u : ℝ := -(2 * Real.pi * ((fam.mesh N).charge : ℝ)) / (8 * (n.val + 1) : ℝ)
 154  phiCostLinearCoeff |u| *
 155      ∑ j : Fin (8 * (n.val + 1)),
 156        |((fam.mesh N).rings n).increments j - u| +
 157    phiCostQuadraticCoeff |u| *
 158      ∑ j : Fin (8 * (n.val + 1)),
 159        (((fam.mesh N).rings n).increments j - u) ^ 2
 160
 161/-- Quantitative perturbation control for a realized sampled family.
 162
 163The `small` field says each sampled increment stays within the unit-scale
 164perturbative regime of `phiCost` once expressed as
 165
 166`Δ_j = (pure winding increment) + ε_j`.
 167
 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. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.