QuantitativeLocalFactorization

formal source

 266uniform bound `M` on the logarithmic derivative `|g'/g|` of the regular
 267factor over the disk. This is the analytic input that controls the
 268phase perturbation `ε_j` on sampled circles. -/
 269structure QuantitativeLocalFactorization extends LocalMeromorphicWitness where
 270  logDerivBound : ℝ
 271  logDerivBound_pos : 0 < logDerivBound
 272  perturbation_regime : logDerivBound * radius ≤ 1
 273
 274/-- On a circle of radius `r` centered at `w.center`, adjacent sample
 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) =