`regular_perturbation_small`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
domain: NumberTheory
line: 196 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 196.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 193
 194/-- The perturbation term lies in the unit-scale regime required by the proved
 195`phiCost` perturbation lemma. -/
 196theorem regular_perturbation_small
 197    {dpf : DefectPhaseFamily} (hw : DefectPhasePerturbationWitness dpf)
 198    (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
 199    |Real.log Constants.phi * hw.epsilon n hn j| ≤ 1 :=
 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

papers checked against this theorem

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