phaseIncrementEpsilonBound

formal source

 275points at angular spacing `2π/(8n)` are separated by arc length
 276`2πr/(8n)`. If the regular factor has log-derivative bounded by `M`,
 277then each phase perturbation satisfies `|ε_j| ≤ M · 2πr/(8n)`. -/
 278noncomputable def phaseIncrementEpsilonBound
 279    (qlf : QuantitativeLocalFactorization) (r : ℝ) (n : ℕ) : ℝ :=
 280  qlf.logDerivBound * (2 * Real.pi * r) / (8 * n)
 281
 282/-- The ε bound is nonneg when r and n are positive. -/
 283theorem phaseIncrementEpsilonBound_nonneg
 284    (qlf : QuantitativeLocalFactorization)
 285    {r : ℝ} (hr : 0 ≤ r) {n : ℕ} (hn : 0 < n) :
 286    0 ≤ phaseIncrementEpsilonBound qlf r n := by
 287  unfold phaseIncrementEpsilonBound
 288  apply div_nonneg
 289  · exact mul_nonneg (le_of_lt qlf.logDerivBound_pos)
 290      (mul_nonneg (mul_nonneg (by positivity : (0:ℝ) ≤ 2) Real.pi_nonneg) hr)
 291  · positivity
 292
 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 -/