 319
 320Once proved, `realizedDefectCostBounded_iff_charge_zero_and_excessBounded`
 321shows that Axiom 2 reduces exactly to forcing zero charge. -/
 322noncomputable def canonicalDefectSampledFamily_ringPerturbationControl
 323    (sensor : DefectSensor) (hm : sensor.charge ≠ 0) :
 324    RingPerturbationControl (canonicalDefectSampledFamily sensor hm) := by
 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,

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.