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

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

  57theorem intensityAtRung_strictly_decreasing (k : ℕ) :
  58    intensityAtRung (k + 1) < intensityAtRung k := by

proof body

Tactic-mode proof.

  59  rw [intensityAtRung_succ_ratio]
  60  have hk : 0 < intensityAtRung k := intensityAtRung_pos k
  61  have hphi_inv_lt_one : phi⁻¹ < 1 := by
  62    have hphi_gt_one : (1 : ℝ) < phi := by
  63      have := Constants.phi_gt_onePointFive; linarith
  64    exact inv_lt_one_of_one_lt₀ hphi_gt_one
  65  have : intensityAtRung k * phi⁻¹ < intensityAtRung k * 1 :=
  66    mul_lt_mul_of_pos_left hphi_inv_lt_one hk
  67  simpa using this
  68

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.