The ratio of consecutive Fibonacci numbers #
We prove that the ratio of consecutive Fibonacci numbers tends to the golden ratio.
theorem
tendsto_fib_succ_div_fib_atTop :
Filter.Tendsto (fun (n : ℕ) => ↑(Nat.fib (n + 1)) / ↑(Nat.fib n)) Filter.atTop (nhds Real.goldenRatio)
The limit of fib (n + 1) / fib n
as n → ∞
is the golden ratio.
theorem
tendsto_fib_div_fib_succ_atTop :
Filter.Tendsto (fun (n : ℕ) => ↑(Nat.fib n) / ↑(Nat.fib (n + 1))) Filter.atTop (nhds (-Real.goldenConj))
The limit of fib n / fib (n + 1)
as n → ∞
is the negative conjugate of the golden ratio.