GeneralizedContinuedFraction.IntFractPair.of_inv_fr_num_lt_num_of_pos
theorem GeneralizedContinuedFraction.IntFractPair.of_inv_fr_num_lt_num_of_pos :
∀ {q : ℚ}, 0 < q → (GeneralizedContinuedFraction.IntFractPair.of q⁻¹).fr.num < q.num
This theorem demonstrates that for any rational number `q` that is greater than `0` and less than `1`, the numerator of the fractional part of the reciprocal of `q` (computed using `GeneralizedContinuedFraction.IntFractPair.of` function) is less than the numerator of `q` itself. In mathematical terms, for `0 < q < 1`, the inequality `numerator(fract(1/q)) < numerator(q)` holds true. The `IntFractPair.of` function is used to create a pair of the integer and fractional part of a number, where the fractional part is represented in terms of its numerator.
More concisely: For any rational number 0 < q < 1, the numerator of the fractional part of 1/q is strictly less than the numerator of q.
|
GeneralizedContinuedFraction.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_rat
theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_rat :
∀ {q : ℚ} {n : ℕ} {ifp_n ifp_succ_n : GeneralizedContinuedFraction.IntFractPair ℚ},
GeneralizedContinuedFraction.IntFractPair.stream q n = some ifp_n →
GeneralizedContinuedFraction.IntFractPair.stream q (n + 1) = some ifp_succ_n →
ifp_succ_n.fr.num < ifp_n.fr.num
This theorem shows that the sequence of numerators of the fractional parts of a generalized continued fraction is strictly decreasing. More precisely, for any rational number `q` and any natural number `n`, if `ifp_n` is the `n`-th element of the stream produced by `GeneralizedContinuedFraction.IntFractPair.stream q n` and `ifp_succ_n` is the `(n+1)`-th element of the same stream, then the numerator of the fractional part of `ifp_succ_n` is strictly less than the numerator of the fractional part of `ifp_n`.
More concisely: For any rational number `q` and natural number `n`, the numerator of the fractional part of the `(n+1)`-th element in the generalized continued fraction of `q` is strictly less than the numerator of the fractional part of the `n`-th element.
|
GeneralizedContinuedFraction.terminates_of_rat
theorem GeneralizedContinuedFraction.terminates_of_rat : ∀ (q : ℚ), (GeneralizedContinuedFraction.of q).Terminates := by
sorry
This theorem states that the generalized continued fraction of any rational number terminates. In other words, for any rational number 'q', the algorithm to compute the generalized continued fraction representation of 'q' will always reach an end point and not continue indefinitely. This is an inherent property of rational numbers in the context of continued fractions.
More concisely: Every rational number has a terminating generalized continued fraction representation.
|
GeneralizedContinuedFraction.coe_of_rat_eq
theorem GeneralizedContinuedFraction.coe_of_rat_eq :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {q : ℚ},
v = ↑q →
{ h := ↑(GeneralizedContinuedFraction.of q).h,
s :=
Stream'.Seq.map (GeneralizedContinuedFraction.Pair.map Rat.cast) (GeneralizedContinuedFraction.of q).s } =
GeneralizedContinuedFraction.of v
The theorem `GeneralizedContinuedFraction.coe_of_rat_eq` states that for any type `K` that is a linearly ordered field and a floor ring, given any value `v` of type `K` and any rational number `q`, if `v` is equal to the cast of `q` into `K`, then the generalized continued fraction of `q` cast into `K` is equal to the generalized continued fraction of `v`. In simpler terms, it asserts the equality of generalized continued fractions after casting a rational number to another numeric type. Here, the casting process involves mapping a function `Rat.cast` over the sequence that represents the continued fraction.
More concisely: For any linearly ordered field and floor ring `K`, if `v` is the cast of rational number `q` into `K`, then the generalized continued fractions of `v` and `q` are equal.
|
GeneralizedContinuedFraction.terminates_iff_rat
theorem GeneralizedContinuedFraction.terminates_iff_rat :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K),
(GeneralizedContinuedFraction.of v).Terminates ↔ ∃ q, v = ↑q
The theorem `GeneralizedContinuedFraction.terminates_iff_rat` states that for any type `K` which is a linearly ordered field and has a floor ring structure, a given value `v` of type `K` represents a terminating continued fraction, denoted by `GeneralizedContinuedFraction.of v`, if and only if `v` is a rational number. In more mathematical terms, `v` can be represented as the quotient of two integers.
More concisely: For any linearly ordered field `K` with a floor ring structure, a value `v` in `K` is the quotient of two integers if and only if `v` has a terminating continued fraction representation in `K`.
|
GeneralizedContinuedFraction.exists_rat_eq_of_terminates
theorem GeneralizedContinuedFraction.exists_rat_eq_of_terminates :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K},
(GeneralizedContinuedFraction.of v).Terminates → ∃ q, v = ↑q
This theorem states that for every terminating generalized continued fraction that generates a value 'v' in a linearly ordered field 'K' (with 'K' also assumed to be a floor ring), there exists a rational number 'q' such that 'v' equates to the field representation of 'q'. In simpler words, it states that any terminating continued fraction corresponds to a specific rational number.
More concisely: Every terminating generalized continued fraction in a linearly ordered field with the property of being a floor ring defines a unique rational number.
|
GeneralizedContinuedFraction.exists_rat_eq_nth_convergent
theorem GeneralizedContinuedFraction.exists_rat_eq_nth_convergent :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K) (n : ℕ),
∃ q, (GeneralizedContinuedFraction.of v).convergents n = ↑q
This theorem states that for any linearly ordered field `K` with a floor ring structure, and for any element `v` of `K` and natural number `n`, there exists a rational number `q` such that the `n`th convergent of the generalized continued fraction representation of `v` is equal to `q`. In simpler terms, this theorem asserts that every finite convergent of a generalized continued fraction can be represented as a rational number.
More concisely: For any linearly ordered field `K` with a floor ring structure and any `v` in `K` and natural number `n`, there exists a rational number `q` such that the `n`-th convergent of `v`'s generalized continued fraction representation equals `q`.
|