English
Let gp = (a_n, b_n) be the nth coefficient pair, and suppose B_n = B_n and B_{n+1} = B_{n+1} denote the denominators. Then B_{n+2} = b_n B_{n+1} + a_n B_n.
Русский
Пусть gp = (a_n, b_n) — n-ая пара коэффициентов, а B_n, B_{n+1} — знаменатели соответствующих континуантов. Тогда B_{n+2} = b_n B_{n+1} + a_n B_n.
LaTeX
$$$B_{n+2} = b_n B_{n+1} + a_n B_n$$$
Lean4
/-- Shows that `Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂`. -/
theorem dens_recurrence {gp : Pair K} {ppredB predB : K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_den_eq : g.dens n = ppredB) (succ_nth_den_eq : g.dens (n + 1) = predB) :
g.dens (n + 2) = gp.b * predB + gp.a * ppredB :=
by
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.b = ppredB :=
exists_conts_b_of_den nth_den_eq
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts (n + 1) = conts ∧ conts.b = predB :=
exists_conts_b_of_den succ_nth_den_eq
rw [den_eq_conts_b, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
