English
Let g be a generalized continued fraction with coefficient pairs (a_n, b_n). If, at position n, the next partial pair is gp = (a_n, b_n) and the current continuants are conts n = (A_n, B_n) and conts n+1 = (A_{n+1}, B_{n+1}), then the continuant at position n+2 is determined by the same linear recurrence: (A_{n+2}, B_{n+2}) = (b_n A_{n+1} + a_n A_n, b_n B_{n+1} + a_n B_n).
Русский
Пусть g — обобщённое непрерывное дробление с парами коэффициентов (a_n, b_n). Если на позиции n следующий член имеет пару gp = (a_n, b_n), а текущие континуанты равны conts n = (A_n, B_n) и conts n+1 = (A_{n+1}, B_{n+1}), тогда континиант на позиции n+2 удовлетворяет тем же линейным рекуррентным отношениям: (A_{n+2}, B_{n+2}) = (b_n A_{n+1} + a_n A_n, b_n B_{n+1} + a_n B_n).
LaTeX
$$$$(A_{n+2},\\, B_{n+2}) = (b_n A_{n+1} + a_n A_n,\\; b_n B_{n+1} + a_n B_n).$$$$
Lean4
/-- Shows that `Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂` and `Bₙ = bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂`. -/
theorem conts_recurrence {gp ppred pred : Pair K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_conts_eq : g.conts n = ppred) (succ_nth_conts_eq : g.conts (n + 1) = pred) :
g.conts (n + 2) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩ :=
by
rw [nth_cont_eq_succ_nth_contAux] at nth_conts_eq succ_nth_conts_eq
exact conts_recurrenceAux succ_nth_s_eq nth_conts_eq succ_nth_conts_eq
