regular_perturbation_linear_term_bounded

formal source

 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)| *
 218          ∑ j : Fin (8 * (n.val + 1)),
 219            (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 ≤ K :=
 220  hw.quadratic_term_bounded
 221
 222/-- A zero-perturbation witness for the trivial defect phase family. -/
 223noncomputable def trivialDefectPhasePerturbationWitness (sensor : DefectSensor) :
 224    DefectPhasePerturbationWitness (trivialDefectPhaseFamily sensor) where
 225  epsilon := fun _ _ _ => 0
 226  increment_eq := by
 227    intro n hn j
 228    dsimp [trivialDefectPhaseFamily, pureDefectPhaseData, defectPhasePureIncrement,
 229      ContinuousPhaseData.sampleIncrements]
 230    have hnR : (8 * (n : ℝ)) ≠ 0 := by
 231      have hnR' : 0 < (n : ℝ) := by
 232        exact_mod_cast hn
 233      nlinarith