pith. machine review for the scientific record. sign in
theorem proved term proof

regular_perturbation_quadratic_term_bounded

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)

 213theorem regular_perturbation_quadratic_term_bounded
 214    {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf) :
 215    ∃ K : ℝ, ∀ N : ℕ,
 216      ∑ n : Fin N,
 217        phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 218          ∑ j : Fin (8 * (n.val + 1)),
 219            (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 ≤ K :=

proof body

Term-mode proof.

 220  hw.quadratic_term_bounded
 221
 222/-- A zero-perturbation witness for the trivial defect phase family. -/

used by (2)

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

depends on (14)

Lean names referenced from this declaration's body.