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

DefectPhasePerturbationWitness

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)

 167structure DefectPhasePerturbationWitness (dpf : DefectPhaseFamily) where
 168  epsilon : (n : ℕ) → 0 < n → Fin (8 * n) → ℝ
 169  increment_eq : ∀ n hn j,
 170    (dpf.phaseAtLevel n hn).sampleIncrements n j =
 171      defectPhasePureIncrement dpf n + epsilon n hn j
 172  small : ∀ n hn j,
 173    |Real.log Constants.phi * epsilon n hn j| ≤ 1
 174  linear_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
 175    ∑ n : Fin N,
 176      phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 177        ∑ j : Fin (8 * (n.val + 1)),
 178          |epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K
 179  quadratic_term_bounded : ∃ K : ℝ, ∀ N : ℕ,
 180    ∑ n : Fin N,
 181      phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 182        ∑ j : Fin (8 * (n.val + 1)),
 183          (epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 ≤ K
 184
 185/-- Each sampled increment decomposes as the pure winding increment plus the
 186regular perturbation provided by the witness. -/

used by (15)

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

depends on (10)

Lean names referenced from this declaration's body.