canonicalDefectSampledFamily_ringPerturbationControl

proof body

Definition body.

 325  let dpf := chosenDefectPhaseFamily sensor hm
 326  let hw := chosenDefectPhasePerturbationWitness sensor hm
 327  refine { small := ?_, total_bounded := ?_ }
 328  · intro N n j
 329    have hsmall := regular_perturbation_small hw (n.val + 1) (Nat.succ_pos n.val) j
 330    have hinc :
 331        (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
 332          defectPhasePureIncrement dpf (n.val + 1) +
 333            hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 334      simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
 335        defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
 336        regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 337    have hpure :
 338        defectPhasePureIncrement dpf (n.val + 1) =
 339          -(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 340            (8 * (n.val + 1) : ℝ) := by
 341      simp [defectPhasePureIncrement, canonicalDefectSampledFamily_charge,
 342        chosenDefectPhaseFamily_sensor, dpf]
 343    rw [hinc, hpure]
 344    simpa using hsmall
 345  obtain ⟨K₁, hK₁⟩ := regular_perturbation_linear_term_bounded hw
 346  obtain ⟨K₂, hK₂⟩ := regular_perturbation_quadratic_term_bounded hw
 347  refine ⟨K₁ + K₂, ?_⟩
 348  intro N
 349  have hlin := hK₁ N
 350  have hquad := hK₂ N
 351  have hterm :
 352      ∀ n : Fin N,
 353        realizedRingPerturbationError (canonicalDefectSampledFamily sensor hm) N n =
 354          phiCostLinearCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 355            ∑ j : Fin (8 * (n.val + 1)),
 356              |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| +
 357          phiCostQuadraticCoeff |defectPhasePureIncrement dpf (n.val + 1)| *
 358            ∑ j : Fin (8 * (n.val + 1)),
 359              (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
 360    intro n
 361    dsimp [realizedRingPerturbationError]
 362    have hpure :
 363        defectPhasePureIncrement dpf (n.val + 1) =
 364          -(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 365            (8 * (n.val + 1) : ℝ) := by
 366      simp [defectPhasePureIncrement, canonicalDefectSampledFamily_charge,
 367        chosenDefectPhaseFamily_sensor, dpf]
 368    rw [hpure]
 369    have hlinSum :
 370        ∑ j : Fin (8 * (n.val + 1)),
 371          |(((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j -
 372            (-(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 373              (8 * (n.val + 1) : ℝ))| =
 374        ∑ j : Fin (8 * (n.val + 1)),
 375          |hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j| := by
 376      apply Finset.sum_congr rfl
 377      intro j _
 378      have hinc :
 379          (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
 380            defectPhasePureIncrement dpf (n.val + 1) +
 381              hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 382        simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
 383          defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
 384          regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 385      rw [hinc, hpure]
 386      ring_nf
 387    have hquadSum :
 388        ∑ j : Fin (8 * (n.val + 1)),
 389          ((((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j -
 390            (-(2 * Real.pi * (((canonicalDefectSampledFamily sensor hm).mesh N).charge : ℝ)) /
 391              (8 * (n.val + 1) : ℝ))) ^ 2 =
 392        ∑ j : Fin (8 * (n.val + 1)),
 393          (hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j) ^ 2 := by
 394      apply Finset.sum_congr rfl
 395      intro j _
 396      have hinc :
 397          (((canonicalDefectSampledFamily sensor hm).mesh N).rings n).increments j =
 398            defectPhasePureIncrement dpf (n.val + 1) +
 399              hw.epsilon (n.val + 1) (Nat.succ_pos n.val) j := by
 400        simpa [canonicalDefectSampledFamily, chosenDefectPhaseFamily, dpf,
 401          defectAnnularMesh, ContinuousPhaseData.toAnnularRingSample] using
 402          regular_factor_increment_decomposition hw (n.val + 1) (Nat.succ_pos n.val) j
 403      rw [hinc, hpure]
 404      ring_nf
 405-- ... 28 more lines elided ...