GeneralizedContinuedFraction.squashSeq_nth_of_not_terminated
theorem GeneralizedContinuedFraction.squashSeq_nth_of_not_terminated :
∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)} [inst : DivisionRing K]
{gp_n gp_succ_n : GeneralizedContinuedFraction.Pair K},
s.get? n = some gp_n →
s.get? (n + 1) = some gp_succ_n →
(GeneralizedContinuedFraction.squashSeq s n).get? n =
some { a := gp_n.a, b := gp_n.b + gp_succ_n.a / gp_succ_n.b }
This theorem states that for any type `K` with a division ring structure, for any natural number `n`, and for any sequence `s` of pairs of generalized continued fractions, if the sequence `s` has not terminated before the position `n + 1`, then after applying the `squashSeq` function at position `n`, the value at position `n` in the modified sequence is equal to a pair whose first component is the first component of the `n`-th pair in the original sequence, and whose second component is the sum of the second component of the `n`-th pair in the original sequence and the ratio of the first component to the second component of the `(n + 1)`-th pair in the original sequence. In other words, if the sequence is not terminated before `n + 1`, the value at `n + 1` gets "squashed" into position `n`.
More concisely: For any type `K` with a division ring structure and any infinite continued fraction sequence `s` in `K × K`, the value at position `n` in the sequence after applying `squashSeq` is equal to the first component of the `n`-th pair and the sum of the second component of the `n`-th pair and the quotient of the first component to the second component of the `(n + 1)`-th pair in the original sequence.
|
GeneralizedContinuedFraction.succ_nth_convergent_eq_squashGCF_nth_convergent
theorem GeneralizedContinuedFraction.succ_nth_convergent_eq_squashGCF_nth_convergent :
∀ {K : Type u_1} {n : ℕ} {g : GeneralizedContinuedFraction K} [inst : Field K],
(∀ {b : K}, g.partialDenominators.get? n = some b → b ≠ 0) →
g.convergents (n + 1) = (g.squashGCF n).convergents n
This theorem states that for any field `K` and any natural number `n`, given a generalized continued fraction `g` over `K`, if the partial denominator at the `n`th position of the generalized continued fraction is not zero, then the `n+1`th convergent of `g` is equal to the `n`th convergent of the squashed generalized continued fraction at the `n`th position. Essentially, this theorem asserts the convergence behavior of a generalized continued fraction under the condition of non-zero partial denominators.
More concisely: For any field `K` and natural number `n`, if the `n`th partial denominator of a generalized continued fraction `g` over `K` is non-zero, then the `(n+1)`th convergent of `g` equals the `n`th convergent of the squashed continued fraction of `g` at position `n`.
|
GeneralizedContinuedFraction.convergents_eq_convergents'
theorem GeneralizedContinuedFraction.convergents_eq_convergents' :
∀ {K : Type u_1} {n : ℕ} {g : GeneralizedContinuedFraction K} [inst : LinearOrderedField K],
(∀ {gp : GeneralizedContinuedFraction.Pair K} {m : ℕ}, m < n → g.s.get? m = some gp → 0 < gp.a ∧ 0 < gp.b) →
g.convergents n = g.convergents' n
This theorem states that for any generalized continued fraction `g` and a natural number `n`, if all the fractions in the sequence of `g` up to `n` have strictly positive values, then the `n`th value of the recurrence relation `convergents` and the direct evaluation `convergents'` of `g` are equal. This condition of positivity is not the only one that can give this result; for instance, sequences with strictly negative values would also work. This theorem is particularly useful when working with regular continued fractions, which inherently satisfy this positivity criterion.
More concisely: For any generalized continued fraction `g` and natural number `n`, if all the convergents of `g` up to `n` have strictly positive values, then the `n`th convergent of `g` according to the recurrence relation and the direct evaluation are equal.
|
GeneralizedContinuedFraction.continuantsAux_eq_continuantsAux_squashGCF_of_le
theorem GeneralizedContinuedFraction.continuantsAux_eq_continuantsAux_squashGCF_of_le :
∀ {K : Type u_1} {n : ℕ} {g : GeneralizedContinuedFraction K} [inst : DivisionRing K] {m : ℕ},
m ≤ n → g.continuantsAux m = (g.squashGCF n).continuantsAux m
This theorem states that for any division ring `K`, natural number `n`, generalized continued fraction `g`, and natural number `m`, if `m` is less than or equal to `n`, then the `m`-th auxiliary continuant of `g` is equal to the `m`-th auxiliary continuant of the squashed form of `g` at position `n`. In other words, squashing a generalized continued fraction does not change the auxiliary continuants before the position where the squashing happens.
More concisely: For any division ring `K`, natural numbers `n` and `m` with `m <= n`, the `m`-th auxiliary continuant of a generalized continued fraction `g` equals the `m`-th auxiliary continuant of its squashed form at position `n`.
|
GeneralizedContinuedFraction.squashGCF_nth_of_lt
theorem GeneralizedContinuedFraction.squashGCF_nth_of_lt :
∀ {K : Type u_1} {n : ℕ} {g : GeneralizedContinuedFraction K} [inst : DivisionRing K] {m : ℕ},
m < n → (g.squashGCF (n + 1)).s.get? m = g.s.get? m
The theorem `GeneralizedContinuedFraction.squashGCF_nth_of_lt` states that for any type `K` with a division ring structure, any natural number `n`, any generalized continued fraction `g` of type `K`, and any natural number `m` such that `m` is less than `n`, the `m`-th value of the sequence obtained by squashing the generalized continued fraction `g` at position `n + 1` is equal to the `m`-th value of the sequence of `g`. In simpler terms, this theorem states that squashing a generalized continued fraction at a certain position doesn't change the values of the sequence before that position.
More concisely: For any type `K` with a division ring structure, any natural numbers `n` and `m` with `m < n`, and any generalized continued fraction `g` of type `K`, the `m`-th squashed value of `g` at position `n+1` equals the `m`-th value of `g`.
|
ContinuedFraction.convergents_eq_convergents'
theorem ContinuedFraction.convergents_eq_convergents' :
∀ {K : Type u_1} [inst : LinearOrderedField K] {c : ContinuedFraction K}, (↑↑c).convergents = (↑↑c).convergents'
The theorem `ContinuedFraction.convergents_eq_convergents'` states that for any regular continued fraction (denoted by `c`) over a linearly ordered field `K`, the sequence of convergents obtained by applying the recurrence relation (`convergents`) is the same as the sequence of convergents obtained through direct evaluation (`convergents'`). In other words, both methods of generating the sequence of convergents for a continued fraction yield the same result.
More concisely: For any regular continued fraction over a linearly ordered field, the sequences of convergents obtained via the recurrence relation and direct evaluation are equal.
|
GeneralizedContinuedFraction.squashSeq_eq_self_of_terminated
theorem GeneralizedContinuedFraction.squashSeq_eq_self_of_terminated :
∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)} [inst : DivisionRing K],
s.TerminatedAt (n + 1) → GeneralizedContinuedFraction.squashSeq s n = s
The theorem `GeneralizedContinuedFraction.squashSeq_eq_self_of_terminated` states that for any type `K` with a division ring structure, any natural number `n`, and any sequence `s` of pairs in the generalized continued fraction of `K`, if the sequence `s` is already terminated at position `n + 1`, then the squashed sequence at position `n` is equal to the original sequence `s`. That is, in such a case, squashing has no effect on the sequence.
More concisely: For any type `K` with a division ring structure, if `s` is a terminated generalized continued fraction sequence of `K` at position `n+1`, then the squashed sequence `s[0..n]` is equal to `s`.
|
GeneralizedContinuedFraction.succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq
theorem GeneralizedContinuedFraction.succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq :
∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)} [inst : DivisionRing K],
GeneralizedContinuedFraction.convergents'Aux s (n + 2) =
GeneralizedContinuedFraction.convergents'Aux (GeneralizedContinuedFraction.squashSeq s n) (n + 1)
The theorem `GeneralizedContinuedFraction.succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squashSeq` states that for any sequence `s` of type `Stream'.Seq (GeneralizedContinuedFraction.Pair K)` in a division ring `K` and for any natural number `n`, the `n+2`-th term of the sequence of convergents (partial sums) `GeneralizedContinuedFraction.convergents'Aux s` is equal to the `n+1`-th term of the sequence of convergents `GeneralizedContinuedFraction.convergents'Aux` of the squashed sequence `GeneralizedContinuedFraction.squashSeq s n`. In other words, squashing the sequence at position `n` and taking the `n+1`-th convergent yields the same value as taking the `n+2`-th convergent of the original sequence directly. Squashing a sequence typically involves combining two consecutive terms into a single term in a certain way.
More concisely: For any sequence `s` of GeneralizedContinuedFractions in a division ring `K` and natural number `n`, the `(n+2)`-th convergent of `s` equals the `(n+1)`-th convergent of the squashed sequence `s` at position `n`.
|
GeneralizedContinuedFraction.squashGCF_eq_self_of_terminated
theorem GeneralizedContinuedFraction.squashGCF_eq_self_of_terminated :
∀ {K : Type u_1} {n : ℕ} {g : GeneralizedContinuedFraction K} [inst : DivisionRing K],
g.TerminatedAt n → g.squashGCF n = g
This theorem states that for any type `K` with a division ring structure and any natural number `n`, if a Generalized Continued Fraction `g` has already terminated at position `n`, then squashing the Generalized Continued Fraction at `n` doesn't change `g`. In other words, if the computation of the continued fraction is complete at a certain step `n`, any further "squashing" or simplification of the fraction at that point does not modify the fraction.
More concisely: For any type `K` with a division ring structure and any natural number `n`, if a Generalized Continued Fraction `g` has terminated at position `n`, then squashing `g` at position `n` leaves `g` unchanged.
|
GeneralizedContinuedFraction.squashSeq_succ_n_tail_eq_squashSeq_tail_n
theorem GeneralizedContinuedFraction.squashSeq_succ_n_tail_eq_squashSeq_tail_n :
∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)} [inst : DivisionRing K],
(GeneralizedContinuedFraction.squashSeq s (n + 1)).tail = GeneralizedContinuedFraction.squashSeq s.tail n
This theorem states that for any type `K` where `K` is a division ring, any natural number `n`, and any sequence `s` of Generalized Continued Fraction Pairs (based on `K`), squashing the sequence at position `n + 1` and then taking the tail of the sequence is equivalent to first taking the tail of the sequence and then squashing at position `n`. In other words, the order of the operations "squash" and "take tail" does not change the result.
More concisely: For any division ring `K`, given a sequence `s` of Generalized Continued Fraction Pairs based on `K` and a natural number `n`, the sequence obtained by squashing at position `n+1` and taking the tail is equal to the sequence obtained by taking the tail and then squashing at position `n`.
|
GeneralizedContinuedFraction.squashSeq_nth_of_lt
theorem GeneralizedContinuedFraction.squashSeq_nth_of_lt :
∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GeneralizedContinuedFraction.Pair K)} [inst : DivisionRing K] {m : ℕ},
m < n → (GeneralizedContinuedFraction.squashSeq s n).get? m = s.get? m
The theorem `GeneralizedContinuedFraction.squashSeq_nth_of_lt` states that for any division ring `K`, natural numbers `n` and `m`, and a sequence `s` of pairs from the generalized continued fraction of `K`, if `m` is less than `n`, then the `m`-th element of the sequence obtained by applying the `squashSeq` operation at position `n` on `s`, is the same as the `m`-th element of the original sequence `s`. Here, `squashSeq` is an operation that modifies a sequence at a specific position, and the theorem guarantees that the elements before this position remain unaffected.
More concisely: For any division ring K, natural numbers n > m, and sequence s of pairs in the generalized continued fraction of K, the m-th element of the sequence obtained by squashing position n in s is equal to the m-th element of the original sequence s.
|
GeneralizedContinuedFraction.succ_nth_convergent'_eq_squashGCF_nth_convergent'
theorem GeneralizedContinuedFraction.succ_nth_convergent'_eq_squashGCF_nth_convergent' :
∀ {K : Type u_1} {n : ℕ} {g : GeneralizedContinuedFraction K} [inst : DivisionRing K],
g.convergents' (n + 1) = (g.squashGCF n).convergents' n
The theorem `GeneralizedContinuedFraction.succ_nth_convergent'_eq_squashGCF_nth_convergent'` states that for any type `K` that forms a division ring, and for any natural number `n`, the `n + 1`-th convergent of a given generalized continued fraction (gcf) `g` is equal to the `n`-th convergent of the squashed gcf of `g` at position `n`. Here, "squashing" a gcf is a transformation that combines two terms into one, and a "convergent" is a certain approximation to the value of the continued fraction.
More concisely: For any division ring type `K` and a generalized continued fraction `g` in `K`, the `(n + 1)`-th convergent of `g` equals the `n`-th convergent of the squashed version of `g` at position `n`.
|