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

r_orbit_adjacent_ratio

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)

  98theorem r_orbit_adjacent_ratio (r0 : ℝ) (h : 0 < r0) (k : ℕ) :
  99    r_orbit r0 (k + 1) / r_orbit r0 k = phi := by

proof body

Term-mode proof.

 100  have hk : r_orbit r0 k > 0 := r_orbit_pos r0 h k
 101  rw [r_orbit_succ]
 102  field_simp
 103
 104/-- Strict monotonicity: outer rung is strictly farther than inner rung. -/

used by (4)

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

depends on (13)

Lean names referenced from this declaration's body.