English
Let gp = (a_n, b_n) be the nth coefficient pair, and suppose A_n = A_n and A_{n+1} = A_{n+1} denote the numerators. Then A_{n+2} = b_n A_{n+1} + a_n A_n.
Русский
Пусть gp = (a_n, b_n) — n-ая пара коэффициентов, а A_n, A_{n+1} — числители соответствующих континуантов. Тогда A_{n+2} = b_n A_{n+1} + a_n A_n.
LaTeX
$$$A_{n+2} = b_n A_{n+1} + a_n A_n$$$
Lean4
/-- Shows that `Aₙ = bₙ * Aₙ₋₁ + aₙ * Aₙ₋₂`. -/
theorem nums_recurrence {gp : Pair K} {ppredA predA : K} (succ_nth_s_eq : g.s.get? (n + 1) = some gp)
(nth_num_eq : g.nums n = ppredA) (succ_nth_num_eq : g.nums (n + 1) = predA) :
g.nums (n + 2) = gp.b * predA + gp.a * ppredA :=
by
obtain ⟨ppredConts, nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts n = conts ∧ conts.a = ppredA :=
exists_conts_a_of_num nth_num_eq
obtain ⟨predConts, succ_nth_conts_eq, ⟨rfl⟩⟩ : ∃ conts, g.conts (n + 1) = conts ∧ conts.a = predA :=
exists_conts_a_of_num succ_nth_num_eq
rw [num_eq_conts_a, conts_recurrence succ_nth_s_eq nth_conts_eq succ_nth_conts_eq]
