`genuineRegularFactorPhaseAt_logDerivBound`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
domain: NumberTheory
line: 502 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 502.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 499This is the critical identity that connects the analytic input
 500(`QuantitativeLocalFactorization.logDerivBound`) to the phase-level
 501Lipschitz constant, enabling discharge of perturbation-witness bounds. -/
 502theorem genuineRegularFactorPhaseAt_logDerivBound
 503    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
 504    (genuineRegularFactorPhaseAt qlf n hn).logDerivBound =
 505      qlf.logDerivBound * (qlf.radius / (↑n + 1)) := by
 506  rfl
 507
 508/-- Absolute bound on epsilon at level `n`: the perturbation increment
 509is bounded by `M * R * 2π / (8n(n+1))`. -/
 510theorem epsilon_abs_bound
 511    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
 512    |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| ≤
 513      qlf.logDerivBound * (qlf.radius / (↑n + 1)) * (2 * π / (8 * ↑n)) := by
 514  exact (genuineRegularFactorPhaseAt qlf n hn).increment_bound n hn j
 515
 516/-- At the genuine phase family, `|ε| ≤ M * R / (n+1) * π / (4n)`, and
 517with `perturbation_regime` this is `≤ π / (4n(n+1)) ≤ π/8 < 1`.
 518So `|log(φ) * ε| < 1 * 1 = 1`. -/
 519theorem epsilon_log_phi_small
 520    (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) (j : Fin (8 * n)) :
 521    |Real.log Constants.phi *
 522      (genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| ≤ 1 := by
 523  have hn_cast : (1 : ℝ) ≤ ↑n := Nat.one_le_cast.mpr hn
 524  have hMR := qlf.perturbation_regime
 525  have heps := epsilon_abs_bound qlf n hn j
 526  rw [abs_mul]
 527  have hlog_pos : 0 < Real.log Constants.phi :=
 528    Real.log_pos (by linarith [Constants.phi_gt_onePointFive])
 529  rw [abs_of_pos hlog_pos]
 530  have hlog_lt_one : Real.log Constants.phi < 1 := by
 531    have hphi_lt_exp1 : Constants.phi < Real.exp 1 :=
 532      calc Constants.phi < 1.62 := Constants.phi_lt_onePointSixTwo

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.