theorem proved term proof

`phaseIncrementEpsilonBound_nonneg`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 283theorem phaseIncrementEpsilonBound_nonneg
 284    (qlf : QuantitativeLocalFactorization)
 285    {r : ℝ} (hr : 0 ≤ r) {n : ℕ} (hn : 0 < n) :
 286    0 ≤ phaseIncrementEpsilonBound qlf r n := by

proof body

Term-mode proof.

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

depends on (13)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
phaseIncrementEpsilonBound in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder decl_use
QuantitativeLocalFactorization in IndisputableMonolith.NumberTheory.MeromorphicCircleOrder decl_use