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

etaBAt_strictly_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)

  58theorem etaBAt_strictly_decreasing (N : ℕ) :
  59    etaBAt (N + 1) < etaBAt N := by

proof body

Tactic-mode proof.

  60  rw [etaBAt_succ_ratio]
  61  have hk : 0 < etaBAt N := etaBAt_pos N
  62  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  63    have hphi_gt_one : (1 : ℝ) < phi := by
  64      have := Constants.phi_gt_onePointFive; linarith
  65    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  66  have : etaBAt N * phi⁻¹ < etaBAt N * 1 :=
  67    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  68  simpa using this
  69
  70/-- Adjacent-e-fold ratio is exactly 1/φ. -/

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.