phaseIncrementEpsilonBound_nonneg

formal source

 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 -/
 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