phaseFamily_ringPerturbationControl

formal source

  65
  66/-- A perturbation witness for any defect phase family induces the ring-level
  67perturbation-control package needed by the annular-cost machinery. -/
  68noncomputable def phaseFamily_ringPerturbationControl
  69    (dpf : DefectPhaseFamily) (hw : DefectPhasePerturbationWitness dpf) :
  70    RingPerturbationControl (dpf.toSampledFamily) := by
  71  refine { small := ?_, total_bounded := ?_ }
  72  · intro N n j
  73    have hsmall := regular_perturbation_small hw (n.val + 1) (Nat.succ_pos n.val) j
  74    have hinc :
  75        (((dpf.toSampledFamily).mesh N).rings n).increments j =
  76          defectPhasePureIncrement dpf (n.val + 1) +
  77            hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
  78      simpa [DefectPhaseFamily.toSampledFamily, defectAnnularMesh,
  79        ContinuousPhaseData.toAnnularRingSample] using
  80        regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
  81    have hpure :
  82        defectPhasePureIncrement dpf (n.val + 1) =
  83          -(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
  84            (8 * (n.val + 1) : ℝ) := by
  85      simp [defectPhasePureIncrement, DefectPhaseFamily.toSampledFamily,
  86        defectAnnularMesh]
  87    rw [hinc, hpure]
  88    simpa using hsmall
  89  obtain ⟨K₁, hK₁⟩ := regular_perturbation_linear_term_bounded hw
  90  obtain ⟨K₂, hK₂⟩ := regular_perturbation_quadratic_term_bounded hw
  91  refine ⟨K₁ + K₂, ?_⟩
  92  intro N
  93  have hterm :
  94      ∀ n : Fin N,
  95        realizedRingPerturbationError (dpf.toSampledFamily) N n =
  96          phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
  97            ∑ j : Fin (8 * (n.val + 1)),
  98              |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +