conts_recurrenceAux — Mathlib

English

A simplified auxiliary recurrence for conts: conts(n+1) equals a linear combination of pred and ppred given previous terms.

Русский

Упрощённая вспомогательная рекуррентность conts: conts(n+1) — линейная комбинация pred и ppred при условии предыдущих членов.

LaTeX

$$$g.conts(n+1) = ⟨gp.b pred.a + gp.a ppred.a, gp.b pred.b + gp.a ppred.b⟩$$$

Lean4

theorem conts_recurrenceAux {gp ppred pred : Pair K} (nth_s_eq : g.s.get? n = some gp)
    (nth_contsAux_eq : g.contsAux n = ppred) (succ_nth_contsAux_eq : g.contsAux (n + 1) = pred) :
    g.conts (n + 1) = ⟨gp.b * pred.a + gp.a * ppred.a, gp.b * pred.b + gp.a * ppred.b⟩ := by
  simp [nth_cont_eq_succ_nth_contAux, contsAux_recurrence nth_s_eq nth_contsAux_eq succ_nth_contsAux_eq]

Похожие утверждения