GeneralizedContinuedFraction.denominators_recurrence
theorem GeneralizedContinuedFraction.denominators_recurrence :
∀ {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [inst : DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K} {ppredB predB : K},
g.s.get? (n + 1) = some gp →
g.denominators n = ppredB →
g.denominators (n + 1) = predB → g.denominators (n + 2) = gp.b * predB + gp.a * ppredB
This theorem states that for any generalized continued fraction `g`, any natural number `n`, and any elements `gp`, `ppredB`, and `predB` of a division ring `K`, if the (n+1)th element of the sequence `g.s` is `gp`, the nth and (n+1)th denominators of `g` are `ppredB` and `predB` respectively, then the (n+2)th denominator of `g` is equal to `bₙ * Bₙ₋₁ + aₙ * Bₙ₋₂`, where `bₙ` and `aₙ` are the components of `gp`. Essentially, it's expressing a recurrence relation for the denominators of a generalized continued fraction in terms of the fraction's sequence elements.
More concisely: For any generalized continued fraction `g` in a division ring `K`, if the (n+1)th element is `gp` with components `b_n` and `a_n`, then the sequence of denominators satisfies `denom(g(n+1)) = b_n * denom(g(n)) + a_n * denom(g(n-1))`.
|
GeneralizedContinuedFraction.continuants_recurrence
theorem GeneralizedContinuedFraction.continuants_recurrence :
∀ {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [inst : DivisionRing K]
{gp ppred pred : GeneralizedContinuedFraction.Pair K},
g.s.get? (n + 1) = some gp →
g.continuants n = ppred →
g.continuants (n + 1) = pred →
g.continuants (n + 2) = { a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }
This theorem establishes a recurrence relation for the continuants in a generalized continued fraction. Given a division ring `K` and a generalized continued fraction `g` of type `K`, for any natural number `n`, and pairs `gp`, `ppred`, `pred` in the continued fraction, if the `n + 1`th element of `g.s` is `gp`, the `n`th continuant of `g` is `ppred`, and the `n + 1`th continuant of `g` is `pred`, then the `n + 2`th continuant of `g` equals `{ a := gp.b * pred.a + gp.a * ppred.a, b := gp.b * pred.b + gp.a * ppred.b }`. In other words, the `a` and `b` values of the `n + 2`th continuant are computed as linear combinations of the `a` and `b` values of the `n` and `n + 1`th continuants, with coefficients from the `n + 1`th element of `g.s`.
More concisely: Given a generalized continued fraction `g` over a division ring `K` and natural number `n`, if the `n+1`th element of `g` is `gp` and the `n`th and `n+1`th continuants are `ppred` and `pred` respectively, then the `n+2`th continuant is `gp.a*pred.a + gp.b*ppred.a` and `gp.a*pred.b + gp.b*ppred.b`.
|
GeneralizedContinuedFraction.numerators_recurrence
theorem GeneralizedContinuedFraction.numerators_recurrence :
∀ {K : Type u_1} {g : GeneralizedContinuedFraction K} {n : ℕ} [inst : DivisionRing K]
{gp : GeneralizedContinuedFraction.Pair K} {ppredA predA : K},
g.s.get? (n + 1) = some gp →
g.numerators n = ppredA → g.numerators (n + 1) = predA → g.numerators (n + 2) = gp.b * predA + gp.a * ppredA
This theorem states that, given an arbitrary type `K` equipped with a division ring structure, a `GeneralizedContinuedFraction` `g` of `K`, a natural number `n`, and three elements of `K` named `gp`, `ppredA`, and `predA`, if the `n + 1`th element of the sequence `g.s` is `gp`, `g`'s `n`th numerator is `ppredA` and `g`'s `n + 1`th numerator is `predA`, then `g`'s `n + 2`th numerator is calculated as `gp.b * predA + gp.a * ppredA`. This is a recurrence relation for the numerators of a generalized continued fraction.
More concisely: Given a generalized continued fraction `g` over a division ring `K`, if `g`'s `n+1`th element is `gp`, `n`th numerator is `ppredA`, and `(n+1)`th numerator is `predA`, then `(n+2)`th numerator is `gp.a * ppredA + gp.b * predA`.
|