phaseFamily_ringPerturbationControl

proof body

Definition body.

  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| +
  99          phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 100            ∑ j : Fin (8 * (n.val + 1)),
 101              (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
 102    intro n
 103    dsimp [realizedRingPerturbationError]
 104    have hpure :
 105        defectPhasePureIncrement dpf (n.val + 1) =
 106          -(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
 107            (8 * (n.val + 1) : ℝ) := by
 108      simp [defectPhasePureIncrement, DefectPhaseFamily.toSampledFamily,
 109        defectAnnularMesh]
 110    rw [hpure]
 111    have hlinSum :
 112        ∑ j : Fin (8 * (n.val + 1)),
 113          |(((dpf.toSampledFamily).mesh N).rings n).increments j -
 114            (-(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
 115              (8 * (n.val + 1) : ℝ))| =
 116        ∑ j : Fin (8 * (n.val + 1)),
 117          |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| := by
 118      apply Finset.sum_congr rfl
 119      intro j _
 120      have hinc :
 121          (((dpf.toSampledFamily).mesh N).rings n).increments j =
 122            defectPhasePureIncrement dpf (n.val + 1) +
 123              hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 124        simpa [DefectPhaseFamily.toSampledFamily, defectAnnularMesh,
 125          ContinuousPhaseData.toAnnularRingSample] using
 126          regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 127      rw [hinc, hpure]
 128      ring_nf
 129    have hquadSum :
 130        ∑ j : Fin (8 * (n.val + 1)),
 131          ((((dpf.toSampledFamily).mesh N).rings n).increments j -
 132            (-(2 * Real.pi * (((dpf.toSampledFamily).mesh N).charge : ℝ)) /
 133              (8 * (n.val + 1) : ℝ))) ^ 2 =
 134        ∑ j : Fin (8 * (n.val + 1)),
 135          (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
 136      apply Finset.sum_congr rfl
 137      intro j _
 138      have hinc :
 139          (((dpf.toSampledFamily).mesh N).rings n).increments j =
 140            defectPhasePureIncrement dpf (n.val + 1) +
 141              hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 142        simpa [DefectPhaseFamily.toSampledFamily, defectAnnularMesh,
 143          ContinuousPhaseData.toAnnularRingSample] using
 144          regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 145      rw [hinc, hpure]
 146      ring_nf
 147    rw [hlinSum, hquadSum]
 148  calc
 149    ∑ n : Fin N, realizedRingPerturbationError (dpf.toSampledFamily) N n
 150        = ∑ n : Fin N,
 151-- ... 24 more lines elided ...