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

epsilon_log_phi_small

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)

 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

proof body

Tactic-mode proof.

 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
 550    _ < 4 / 8 := by linarith [Real.pi_lt_four]
 551    _ < 1 := by norm_num
 552
 553/-- Bound on the inner j-sum of |epsilon| at level n+1: the 8(n+1) terms
 554each bounded by `M * R / (n+2) * 2π / (8(n+1))`, summing to ≤ `M * R * 2π / (n+2)`. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (15)

Lean names referenced from this declaration's body.