squashGCF — Mathlib

English

The convergents convs' satisfy a recurrence relation expressing each convs' in terms of previous ones and floor of v.

Русский

Сходящиеся дроби convs' удовлетворяют рекуррентному отношению, выражающему каждое значение через предыдущие и целую часть от v.

LaTeX

$$$(of v).convs' (n+1) = \\lfloor v \\rfloor + 1 / (of Int.fract v)^{-1} .convs' n$$$

Lean4

/-- Given a gcf `g = [h; (a₀, b₀), (a₁, b₁), ...]`, we have
- `squashGCF g 0 = [h + a₀ / b₀; (a₁, b₁), ...]`,
- `squashGCF g (n + 1) = ⟨g.h, squashSeq g.s n⟩`
-/
def squashGCF (g : GenContFract K) : ℕ → GenContFract K
  | 0 =>
    match g.s.get? 0 with
    | none => g
    | some gp => ⟨g.h + gp.a / gp.b, g.s⟩
  | n + 1 => ⟨g.h, squashSeq g.s n⟩

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