English
A formal statement that convs equals convs' under the same positivity hypotheses; the detailed proof relies on induction and the auxiliary stability lemmas for squashed sequences.
Русский
Формальное утверждение, что convs равно convs' при тех же допущениях на положительность; доказательство опирается на индукцию и вспомогательные леммы о стабильности схлопнутых последовательностей.
LaTeX
$$$$\text{If the positivity condition holds } g.convs(n) = g.convs'(n) \text{ for all } n.$$$$
Lean4
/-- Shows that the recurrence relation (`convs`) and direct evaluation (`convs'`) of a
(regular) continued fraction coincide. -/
theorem convs_eq_convs' [Field K] [LinearOrder K] [IsStrictOrderedRing K] {c : ContFract K} :
(↑c : GenContFract K).convs = (↑c : GenContFract K).convs' :=
by
ext n
apply GenContFract.convs_eq_convs'
intro gp m _ s_nth_eq
exact
⟨zero_lt_one.trans_le ((c : SimpContFract K).property m gp.a (partNum_eq_s_a s_nth_eq)).symm.le,
c.property m gp.b <| partDen_eq_s_b s_nth_eq⟩
