GeneralizedContinuedFraction.of_correctness_atTop_of_terminates
theorem GeneralizedContinuedFraction.of_correctness_atTop_of_terminates :
∀ {K : Type u_1} [inst : LinearOrderedField K] {v : K} [inst_1 : FloorRing K],
(GeneralizedContinuedFraction.of v).Terminates →
∀ᶠ (n : ℕ) in Filter.atTop, v = (GeneralizedContinuedFraction.of v).convergents n
The theorem `GeneralizedContinuedFraction.of_correctness_atTop_of_terminates` states the following: For any field `K` that is linearly ordered and any value `v` in `K` (where `K` also holds a `FloorRing` structure), if the generalized continued fraction of `v` terminates, then eventually for all integers `n` greater than a certain threshold (represented by `Filter.atTop` which means as `n` approaches infinity), `v` is equal to the `n`th convergent of the generalized continued fraction of `v`. In other words, if the generalized continued fraction of `v` terminates, the `n`th convergent of the generalized continued fraction of `v` will eventually always be `v` as `n` goes to infinity.
More concisely: For any terminating generalized continued fraction `cf` in a linearly ordered field `K` with a `FloorRing` structure, the `n`th convergent of `cf` approaches `cf`'s limit as `n` approaches infinity.
|
GeneralizedContinuedFraction.of_correctness_of_nth_stream_eq_none
theorem GeneralizedContinuedFraction.of_correctness_of_nth_stream_eq_none :
∀ {K : Type u_1} [inst : LinearOrderedField K] {v : K} {n : ℕ} [inst_1 : FloorRing K],
GeneralizedContinuedFraction.IntFractPair.stream v n = none →
v = (GeneralizedContinuedFraction.of v).convergents (n - 1)
This theorem states that for any linear ordered field `K`, value `v` of type `K`, natural number `n`, and provided `K` is a floor ring, if the `n`-th stream of the `IntFractPair` for the generalized continued fraction of `v` is `none` (i.e., the stream terminates at step `n`), then the value `v` is exactly the `n-1`-th convergent of the generalized continued fraction of `v`.
More concisely: If in the generalized continued fraction representation of a linear ordered field `K`'s element `v`, the `n`-th term is `none`, then `v` equals the `(n-1)`-th convergent of `v`'s continued fraction.
|
GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some
theorem GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some :
∀ {K : Type u_1} [inst : LinearOrderedField K] {v : K} {n : ℕ} [inst_1 : FloorRing K]
{ifp_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n →
v =
GeneralizedContinuedFraction.compExactValue ((GeneralizedContinuedFraction.of v).continuantsAux n)
((GeneralizedContinuedFraction.of v).continuantsAux (n + 1)) ifp_n.fr
This theorem describes the correctness of the `compExactValue` function for a given continued fraction `GeneralizedContinuedFraction.of v` that did not terminate at position `n`. It states that if we have a certain value `v` and we pass the two successive (auxiliary) continuants at positions `n` and `n + 1`, as well as the fractional part at `IntFractPair.stream n` to `compExactValue`, we will correctly obtain the value `v`. This is demonstrated with an example where `v = 3.4` and the fractional term at position `2` is `0.5`, leading to the calculation `v = 3 + 1/(2 + 0.5) = 3 + 1/2.5 = 3.4`. This computation corresponds to the one using the recurrence equation in `compExactValue`.
More concisely: Given a non-terminating continued fraction `GeneralizedContinuedFraction.of v` at position `n`, the function `compExactValue` correctly computes the value `v` using the auxiliary continuants at positions `n` and `n+1` and the fractional part at position `n`.
|
GeneralizedContinuedFraction.of_correctness_of_terminatedAt
theorem GeneralizedContinuedFraction.of_correctness_of_terminatedAt :
∀ {K : Type u_1} [inst : LinearOrderedField K] {v : K} {n : ℕ} [inst_1 : FloorRing K],
(GeneralizedContinuedFraction.of v).TerminatedAt n → v = (GeneralizedContinuedFraction.of v).convergents n
This theorem states that for any number `v` of any linearly ordered field `K` and any natural number `n`, provided that `K` is also a floor ring, if the generalized continued fraction of `v` terminates at step `n`, then the `n`-th convergent of this generalized continued fraction is exactly equal to `v`. In other words, it says that if a generalized continued fraction stops after a certain number of steps, the value at that step is exactly the original number the fraction was representing.
More concisely: For any linearly ordered field `K` that is a floor ring, if the generalized continued fraction of `v` in `K` terminates at step `n`, then the `n`-th convergent equals `v`.
|
GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some_aux_comp
theorem GeneralizedContinuedFraction.compExactValue_correctness_of_stream_eq_some_aux_comp :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {a : K} (b c : K),
Int.fract a ≠ 0 → (↑⌊a⌋ * b + c) / Int.fract a + b = (b * a + c) / Int.fract a
This theorem states that for any type `K` that is a LinearOrderedField and a FloorRing, and for any values `a`, `b`, and `c` of type `K`, if the fractional part of `a` is not zero, then the expression `(floor(a) * b + c) / fractional part of a + b` is equal to `(b * a + c) / fractional part of a`. In other words, it rewrites a formula involving division and addition of values in `K` under the assumption that the fractional part of `a` is non-zero.
More concisely: For any LinearOrderedField and FloorRing `K`, `a`, `b`, `c` in `K` with non-zero fractional part of `a`, we have `(floor(a) * b + c) / (fractional part of a + b) = (b * a + c) / (fractional part of a)`.
|
GeneralizedContinuedFraction.of_correctness_of_terminates
theorem GeneralizedContinuedFraction.of_correctness_of_terminates :
∀ {K : Type u_1} [inst : LinearOrderedField K] {v : K} [inst_1 : FloorRing K],
(GeneralizedContinuedFraction.of v).Terminates → ∃ n, v = (GeneralizedContinuedFraction.of v).convergents n
The theorem `GeneralizedContinuedFraction.of_correctness_of_terminates` states that for any value `v` of a linearly ordered field type `K`, where `K` also has a floor ring structure, if the generalized continued fraction of `v` terminates, there exists a natural number `n` such that the `n`-th convergent of the generalized continued fraction of `v` equals `v` itself. In simple terms, if we can properly represent a number as a finite generalized continued fraction, then this number can be obtained as a convergent of its continued fraction representation.
More concisely: If a number `v` in a linearly ordered field `K` with a floor ring structure has a terminating generalized continued fraction representation, then there exists a natural number `n` such that the `n`-th convergent of the generalized continued fraction equals `v`.
|