theorem
proved
epsilon_log_phi_small
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.MeromorphicCircleOrder on GitHub at line 519.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
radius -
phi_gt_onePointFive -
phi_lt_onePointSixTwo -
Constants -
lt_trans -
of -
of -
of -
of -
epsilon_abs_bound -
genuineRegularFactorPhaseAt -
QuantitativeLocalFactorization -
M -
M
used by
formal source
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
541 _ = qlf.logDerivBound * qlf.radius / (↑n + 1) * (2 * Real.pi / (8 * ↑n)) := by ring
542 _ ≤ 1 / (↑n + 1) * (2 * Real.pi / (8 * ↑n)) := by
543 apply mul_le_mul_of_nonneg_right _ (by positivity)
544 exact div_le_div_of_nonneg_right hMR (by linarith)
545 _ = 2 * Real.pi / (8 * ↑n * (↑n + 1)) := by field_simp
546 _ ≤ 2 * Real.pi / (8 * 1 * 2) := by
547 apply div_le_div_of_nonneg_left (by positivity) (by positivity)
548 nlinarith
549 _ = Real.pi / 8 := by ring