GeneralizedContinuedFraction.zero_le_of_denom
theorem GeneralizedContinuedFraction.zero_le_of_denom :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K],
0 ≤ (GeneralizedContinuedFraction.of v).denominators n
This theorem states that in the context of a linear ordered field `K` and a floor ring `K`, for any value of `v` in `K` and any natural number `n`, the `n`-th denominator of the generalized continued fraction of `v` is always nonnegative. The theorem holds for all types `K`, values `v` of type `K`, and natural numbers `n`.
More concisely: For all linear ordered fields `K` and floor rings `K`, and for all `v` in `K` and natural numbers `n`, the `n`-th denominator of the generalized continued fraction of `v` is nonnegative.
|
GeneralizedContinuedFraction.exists_int_eq_of_part_denom
theorem GeneralizedContinuedFraction.exists_int_eq_of_part_denom :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {b : K},
(GeneralizedContinuedFraction.of v).partialDenominators.get? n = some b → ∃ z, b = ↑z
This theorem states that for any type `K`, value `v` of type `K`, natural number `n`, and `b` of type `K`, with the conditions that `K` is a linearly ordered field and a floor ring, if `b` is a partial denominator of the generalized continued fraction representation of `v` at position `n`, then there exists an integer `z` such that `b` is equal to the real number representation of `z`. Essentially, it guarantees that the partial denominators of a generalized continued fraction are integers.
More concisely: In a linearly ordered field and floor ring `K`, the partial denominators of the generalized continued fraction representation of a value `v` of type `K` at position `n` are integers.
|
GeneralizedContinuedFraction.abs_sub_convergents_le'
theorem GeneralizedContinuedFraction.abs_sub_convergents_le' :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {b : K},
(GeneralizedContinuedFraction.of v).partialDenominators.get? n = some b →
|v - (GeneralizedContinuedFraction.of v).convergents n| ≤
1 /
(b * (GeneralizedContinuedFraction.of v).denominators n *
(GeneralizedContinuedFraction.of v).denominators n)
The theorem `GeneralizedContinuedFraction.abs_sub_convergents_le'` states that for any type `K` which is a linear ordered field and a floor ring, any real number `v`, and any natural number `n`, given that the `n`th value of the partial denominators of the generalized continued fraction of `v` is `b`, the absolute difference between `v` and the `n`th convergent of the generalized continued fraction of `v` is less than or equal to `1` divided by the product of `b` and the square of the `n`th denominator of the generalized continued fraction of `v`. Although this bound is less precise than the one given in `GCF.abs_sub_convergents_le`, it can sometimes be easier to apply and sufficient for certain applications.
More concisely: For any real number `v` with generally convergent generalized continued fraction in a linear ordered field and floor ring, and given the `n`th partial denominator `b` and the `n`th denominator `d`, the absolute difference between `v` and the `n`th convergent is bounded by `1 / (bd^2)`.
|
GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_lt_one
theorem GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_lt_one :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{ifp_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n → ifp_n.fr < 1
This theorem states that the fractional parts of the nth element of a stream of integer-fraction pairs, in any ordered field that has a floor function, are always less than one. Given a type `K` representing an ordered field and another type `GeneralizedContinuedFraction.IntFractPair K` representing pairs of integers and fractions, for any real number `v` and natural number `n`, if the nth element of the integer-fraction pair stream generated by `v` exists and is denoted as `ifp_n`, then the fractional part of `ifp_n` is less than one.
More concisely: For any ordered field `K` and real number `v`, the fractional part of the n-th element in the continued fraction expansion of `v` as an integer-fraction pair, denoted `ifp_n` in `K`, satisfies `0 < ifp_n`.
|
GeneralizedContinuedFraction.of_denom_mono
theorem GeneralizedContinuedFraction.of_denom_mono :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K],
(GeneralizedContinuedFraction.of v).denominators n ≤ (GeneralizedContinuedFraction.of v).denominators (n + 1)
This theorem, `GeneralizedContinuedFraction.of_denom_mono`, states that the sequence of denominators of a generalized continued fraction is monotone, meaning that every term `Bₙ` in the sequence is less than or equal to the next term `Bₙ₊₁`. Here, `K` represents the type of the elements of the sequence, `v` is the value of the generalized continued fraction, and `n` is a natural number representing the position in the sequence. The theorem holds for all `K` that are linearly ordered fields and have a defined floor function.
More concisely: For all linearly ordered fields K with a defined floor function, the sequence of denominators in the generalized continued fraction representation of an element v in K is monotone increasing.
|
GeneralizedContinuedFraction.abs_sub_convergents_le
theorem GeneralizedContinuedFraction.abs_sub_convergents_le :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K],
¬(GeneralizedContinuedFraction.of v).TerminatedAt n →
|v - (GeneralizedContinuedFraction.of v).convergents n| ≤
1 /
((GeneralizedContinuedFraction.of v).denominators n *
(GeneralizedContinuedFraction.of v).denominators (n + 1))
This theorem states that for any type `K` that forms a linear ordered field and a floor ring, and for any value `v` of type `K` and natural number `n`, if the generalized continued fraction of `v` does not terminate at `n`, then the absolute difference between `v` and the `n`th convergent of the generalized continued fraction of `v` is less than or equal to `1` divided by the product of the `n`th and `(n + 1)`th denominators of the generalized continued fraction of `v`.
More concisely: For any linear ordered field and floor ring `K`, any `v` in `K`, and natural number `n`, if the generalized continued fraction of `v` does not terminate at `n`, then the absolute difference between `v` and the `n`th convergent's value is less than or equal to `1 / (n+1) * nth_denominator(v)`.
|
GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_nonneg_lt_one
theorem GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_nonneg_lt_one :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{ifp_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n → 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1
This theorem states that for any type `K` that forms a linearly ordered field and for which a floor operation is defined, for any value `v` of type `K`, and for any natural number `n`, if we generate a stream of integer-fraction pairs from the generalized continued fraction representation of `v` and fetch the `n`th element from this stream (denoted by `ifp_n`), then the fractional part of `ifp_n` is guaranteed to be a non-negative real number that is less than 1.
More concisely: For any linearly ordered field `K` with defined floor operation and element `v`, the `n`-th fraction from the generalized continued fraction representation of `v` has a non-negative and strictly less than 1 fractional part.
|
GeneralizedContinuedFraction.of_part_num_eq_one_and_exists_int_part_denom_eq
theorem GeneralizedContinuedFraction.of_part_num_eq_one_and_exists_int_part_denom_eq :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{gp : GeneralizedContinuedFraction.Pair K},
(GeneralizedContinuedFraction.of v).s.get? n = some gp → gp.a = 1 ∧ ∃ z, gp.b = ↑z
This theorem states that for any field `K` which is linearly ordered and has a floor function, a given generalized continued fraction pair `gp` at position `n` in the continued fraction expansion of a value `v`, the partial numerator `aᵢ` of the pair `gp` equals one and the partial denominator `bᵢ` corresponds to some integer `z`.
More concisely: For any linearly ordered field with a floor function, the n-th generalized continued fraction coefficient of a value has a partial numerator of 1 and a partial denominator equal to some integer.
|
GeneralizedContinuedFraction.of_part_num_eq_one
theorem GeneralizedContinuedFraction.of_part_num_eq_one :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {a : K},
(GeneralizedContinuedFraction.of v).partialNumerators.get? n = some a → a = 1
This theorem states that for any type `K` that is a linearly ordered field and is also a floor ring, any instance `v` of this type, and any natural number `n`, if `a` is the value obtained from getting the `n`th item of the partial numerators of the generalized continued fraction of `v`, then `a` is equal to 1. In other words, it shows that the partial numerators `aᵢ` of any generalized continued fraction representation in such a field are always 1.
More concisely: In a linearly ordered field and floor ring `K`, the partial numerators of any generalized continued fraction representation are equal to 1 for all indices.
|
GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv
theorem GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_b_le_nth_stream_fr_inv :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{ifp_n ifp_succ_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n →
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) = some ifp_succ_n → ↑ifp_succ_n.b ≤ ifp_n.fr⁻¹
This theorem asserts that for any type `K` (where `K` is a linear ordered field and a floor ring), any value `v` of type `K`, any natural number `n`, and any two elements `ifp_n` and `ifp_succ_n` of type `GeneralizedContinuedFraction.IntFractPair K`, if `ifp_n` is the `n`th integer-fraction pair in the generalized continued fraction stream of `v` and `ifp_succ_n` is the `(n + 1)`th pair in the same stream, then the integer part of `ifp_succ_n` is less than or equal to the reciprocal of the fractional part of `ifp_n`. This is an expected result, as the integer part of the `(n + 1)`th pair is defined as the floor of the reciprocal of the fractional part of the `n`th pair.
More concisely: For any linear ordered field `K`, the integer part of the `(n+1)`th integer-fraction pair in the generalized continued fraction expansion of `v` in `K` is less than or equal to the reciprocal of the fractional part of the `n`th pair.
|
GeneralizedContinuedFraction.succ_nth_fib_le_of_nth_denom
theorem GeneralizedContinuedFraction.succ_nth_fib_le_of_nth_denom :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K],
n = 0 ∨ ¬(GeneralizedContinuedFraction.of v).TerminatedAt (n - 1) →
↑(n + 1).fib ≤ (GeneralizedContinuedFraction.of v).denominators n
This theorem states that for any natural number `n`, in a certain context of a linearly ordered field `K` and floor ring `K`, and given a value `v` of `K`, if `n` equals zero or the generalized continued fraction of `v` has not terminated at `n - 1`, then the `n+1`th Fibonacci number is less than or equal to the `n`th denominator of the generalized continued fraction of `v`. In other words, it establishes a bound for the Fibonacci sequence numbers in terms of the denominators of a generalized continued fraction.
More concisely: For any natural number `n` and element `v` in a linearly ordered field `K` with a floor ring, if `n` is zero or the `(n-1)`th term of `v`'s generalized continued fraction is not reached, then `Fib(n+1) ≤ (denominator v_n)`.
|
GeneralizedContinuedFraction.determinant
theorem GeneralizedContinuedFraction.determinant :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K],
¬(GeneralizedContinuedFraction.of v).TerminatedAt n →
(GeneralizedContinuedFraction.of v).numerators n * (GeneralizedContinuedFraction.of v).denominators (n + 1) -
(GeneralizedContinuedFraction.of v).denominators n *
(GeneralizedContinuedFraction.of v).numerators (n + 1) =
(-1) ^ (n + 1)
The theorem `GeneralizedContinuedFraction.determinant` states that for any type `K`, value `v` of type `K`, and natural number `n`, given that `K` forms a linear ordered field and a floor ring, if the generalized continued fraction of `v` does not terminate at `n`, then the determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)` holds. Here, `Aₙ` and `Bₙ` are the numerator and the denominator of the nth term of the generalized continued fraction of `v` respectively.
More concisely: For any linear ordered field and floor ring `K`, if the generalized continued fraction of an element `v` in `K` does not terminate at the `n`th term, then the determinant of the `(n+1)`x`(n+1)` matrices `[A_n | B_{n+1}]` and `[B_n | A_{n+1}]`, where `A_n` and `B_n` are the numerator and denominator of the `n`th term respectively, is equal to `(-1)^(n+1)`.
|
GeneralizedContinuedFraction.of_one_le_get?_part_denom
theorem GeneralizedContinuedFraction.of_one_le_get?_part_denom :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {b : K},
(GeneralizedContinuedFraction.of v).partialDenominators.get? n = some b → 1 ≤ b
This theorem states that for any type `K` that has an order structure (a `LinearOrderedField`) and a `FloorRing` structure, any value `v` of type `K`, and any natural number `n`, if `b` is the `n`th element of the sequence of partial denominators of the generalized continued fraction representation of `v`, then `b` is greater than or equal to 1. In other words, the integer parts of the continued fraction representation of any number are always at least one.
More concisely: For any number `v` in a LinearOrderedField with a FloorRing structure, the integer parts of its generalized continued fraction representation are greater than or equal to 1.
|
GeneralizedContinuedFraction.IntFractPair.one_le_succ_nth_stream_b
theorem GeneralizedContinuedFraction.IntFractPair.one_le_succ_nth_stream_b :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{ifp_succ_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) = some ifp_succ_n → 1 ≤ ifp_succ_n.b
This theorem states that for any linear ordered field `K` and any element `v` of `K`, for any natural number `n`, under the conditions that `K` also has a floor ring structure and `ifp_succ_n` is a pair of integers following some rules (GeneralizedContinuedFraction.IntFractPair), if the `(n+1)`-th element of a certain sequence (stream) derived from `v` is `ifp_succ_n`, then the second component (`b`) of `ifp_succ_n` is at least 1.
More concisely: Given a linear ordered field `K` with a floor ring structure, if for some natural number `n` and element `v` in `K`, the `(n+1)`-th element in the sequence derived from `v` is `ifp_succ_n` with second component `b`, then `b` is at least 1.
|
GeneralizedContinuedFraction.le_of_succ_get?_denom
theorem GeneralizedContinuedFraction.le_of_succ_get?_denom :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {b : K},
(GeneralizedContinuedFraction.of v).partialDenominators.get? n = some b →
b * (GeneralizedContinuedFraction.of v).denominators n ≤
(GeneralizedContinuedFraction.of v).denominators (n + 1)
This theorem shows that for any linearly ordered field `K`, any `v` in `K`, and any natural number `n`, if `b` is the `n`th partial denominator of the generalized continued fraction representation of `v`, then the product of `b` and the `n`th denominator of the continued fraction is less than or equal to the `(n+1)`th denominator of the continued fraction. This is formalized as `b * Bₙ ≤ Bₙ₊₁`, where `Bₙ` and `Bₙ₊₁` are the `n`th and `(n+1)`th denominators of the continued fraction.
More concisely: For any linearly ordered field `K`, the `n`th partial denominator `b` of a continued fraction representation in `K` satisfies the inequality `b * (n+1)th denominator ≤ (n+1)th denominator`.
|
GeneralizedContinuedFraction.sub_convergents_eq
theorem GeneralizedContinuedFraction.sub_convergents_eq :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{ifp : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp →
let g := GeneralizedContinuedFraction.of v;
let B := (g.continuantsAux (n + 1)).b;
let pB := (g.continuantsAux n).b;
v - g.convergents n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
The theorem `GeneralizedContinuedFraction.sub_convergents_eq` states that for any type `K`, any value `v` of type `K`, and any natural number `n`, given `K` is a linear ordered field and `K` is a floor ring, and for any instance `ifp` of `GeneralizedContinuedFraction.IntFractPair K`, if `GeneralizedContinuedFraction.IntFractPair.stream v n` equals `ifp`, then the difference between `v` and the `n`th convergent of the generalized continued fraction of `v` equals 0 if `ifp.fr` equals 0; otherwise, it is equal to `(-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))`, where `g` is the generalized continued fraction of `v`, `B` is the `b` value of the `(n + 1)`th auxiliary continuant of `g`, and `pB` is the `b` value of the `n`th auxiliary continuant of `g`.
More concisely: For any generalized continued fraction `g` over a linear ordered field and floor ring `K`, if `v` is a value of type `K` and `(n, (p, q))` is the `n`th convergent of `g` such that `(v, q)` equals the `IntFractPair` representation of `g`, then `v - p / q` equals `(-1)^n * B / (B * (g⁻¹ * B + pB)`, where `B` is the `b` value of the `(n+1)`th auxiliary continuant of `g`.
|
GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_nonneg
theorem GeneralizedContinuedFraction.IntFractPair.nth_stream_fr_nonneg :
∀ {K : Type u_1} {v : K} {n : ℕ} [inst : LinearOrderedField K] [inst_1 : FloorRing K]
{ifp_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n → 0 ≤ ifp_n.fr
This theorem states that the fractional parts of the `n`-th element of the stream of `GeneralizedContinuedFraction.IntFractPair` of a given value in any linear ordered field and floor ring are always nonnegative. Here, `K` is the type of the elements, `v` is the input value, and `n` is the index of the element in the stream. The theorem ensures that if the `n`-th element of the stream exists (`ifp_n`), its fractional part (`ifp_n.fr`) is greater than or equal to zero.
More concisely: For all linear ordered fields K and any value v in K, the n-th fractional part of the GeneralizedContinuedFraction.IntFractPair of v is nonnegative when it exists.
|