`epsilon_abs_bound`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.MeromorphicCircleOrder
domain: NumberTheory
line: 510 · 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 510.

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

used by

formal source

 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
 533        _ < 2 := by norm_num
 534        _ ≤ Real.exp 1 := by linarith [add_one_le_exp (1 : ℝ)]
 535    exact (Real.log_lt_iff_lt_exp (by linarith [Constants.phi_pos])).mpr hphi_lt_exp1
 536  suffices heps_lt_one :
 537      |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j| < 1 by
 538    exact le_of_lt (lt_trans (mul_lt_of_lt_one_right hlog_pos heps_lt_one) hlog_lt_one)
 539  calc |(genuineRegularFactorPhaseAt qlf n hn).sampleIncrements n j|
 540    ≤ qlf.logDerivBound * (qlf.radius / (↑n + 1)) * (2 * Real.pi / (8 * ↑n)) := heps

papers checked against this theorem

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