phaseIncrementEpsilonBound_decreasing

formal source

 293/-- With decreasing radii `r_n = r₀/(n+1)`, the per-ring ε bound decays
 294as `O(1/n²)`, making the sum of all `|ε_j|` across ring `n` equal to
 295`O(1/n)` (since ring `n` has `8(n+1)` samples). -/
 296theorem phaseIncrementEpsilonBound_decreasing
 297    (qlf : QuantitativeLocalFactorization)
 298    {r₀ : ℝ} (hr₀ : 0 < r₀) (n : ℕ) :
 299    phaseIncrementEpsilonBound qlf (r₀ / (↑n + 1)) (n + 1) =
 300      qlf.logDerivBound * (2 * Real.pi * r₀) / (8 * (↑n + 1) ^ 2) := by
 301  unfold phaseIncrementEpsilonBound
 302  have hn : (0 : ℝ) < (n : ℝ) + 1 := by positivity
 303  field_simp
 304  ring_nf
 305  simp [Nat.cast_add, Nat.cast_one]
 306  ring
 307
 308/-! ### §5. Zeta-derived phase family from meromorphic factorization -/
 309
 310/-- Phase data on the `n`th circle of a meromorphic factorization, at
 311radius `r₀/(n+1)`. Bundles the `ContinuousPhaseData` with a proof that
 312its charge equals `-order`, extracted from `meromorphic_phase_charge`. -/
 313private noncomputable def zetaDerivedPhaseDataBundle
 314    (qlf : QuantitativeLocalFactorization) (n : ℕ) (_hn : 0 < n) :
 315    { cpd : ContinuousPhaseData // cpd.charge = -qlf.order } := by
 316  have hd : (0 : ℝ) < ↑n + 1 := by linarith
 317  refine ⟨{
 318    center := qlf.center
 319    radius := qlf.radius / (↑n + 1)
 320    radius_pos := div_pos qlf.radius_pos hd
 321    phase := fun θ => (qlf.order : ℝ) * θ
 322    phase_continuous := by
 323      simpa using (continuous_const.mul continuous_id)
 324    charge := -qlf.order
 325    phase_winding := by
 326      simp [sub_eq_add_neg, Int.cast_neg]