pith. machine review for the scientific record. sign in
theorem proved tactic proof

phaseIncrementEpsilonBound_decreasing

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

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

depends on (17)

Lean names referenced from this declaration's body.