regular_factor_increment_decomposition

formal source

 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)
 198    (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
 199    |Real.log Constants.phi * hw.epsilon n hn j| ≤ 1 :=
 200  hw.small n hn j
 201
 202/-- Uniform bound for the linear perturbation budget. -/
 203theorem regular_perturbation_linear_term_bounded
 204    {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf) :
 205    ∃ K : ℝ, ∀ N : ℕ,
 206      ∑ n : Fin N,
 207        phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 208          ∑ j : Fin (8 * (n.val + 1)),
 209            |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| ≤ K :=
 210  hw.linear_term_bounded
 211
 212/-- Uniform bound for the quadratic perturbation budget. -/
 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)| *