DefectPhasePerturbationWitness

formal source

 164   `phiCost` bound; and
 1653. the total linear and quadratic perturbation budgets are uniformly bounded in
 166   the refinement depth `N`. -/
 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. -/
 187theorem regular_factor_increment_decomposition
 188    {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)
 189    (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
 190    (dpf.phaseAtLevel n hn).sampleIncrements n j =
 191      defectPhasePureIncrement dpf n + hw.epsilon n hn j :=
 192  hw.increment_eq n hn j
 193
 194/-- The perturbation term lies in the unit-scale regime required by the proved
 195`phiCost` perturbation lemma. -/
 196theorem regular_perturbation_small
 197    {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)