GeneralizedContinuedFraction.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none
theorem GeneralizedContinuedFraction.of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {n : ℕ},
(GeneralizedContinuedFraction.of v).TerminatedAt n ↔
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) = none
This theorem states that for any type `K` which is a linear ordered field and a floor ring, and for any value `v` of type `K` and a natural number `n`, a generalized continued fraction derived from `v` terminates at position `n` if and only if the stream of integer-fraction pairs derived from `v` is `none` at position `n + 1`. In other words, the termination of the generalized continued fraction at a specific position corresponds to the absence of an integer-fraction pair at the next position in the related sequence.
More concisely: A generalized continued fraction for a linear ordered field and floor ring `K` value `v` terminates at position `n` if and only if the sequence of integer-fraction pairs derived from `v` is empty at position `n+1`.
|
GeneralizedContinuedFraction.IntFractPair.stream_zero
theorem GeneralizedContinuedFraction.IntFractPair.stream_zero :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K),
GeneralizedContinuedFraction.IntFractPair.stream v 0 = some (GeneralizedContinuedFraction.IntFractPair.of v)
The theorem `GeneralizedContinuedFraction.IntFractPair.stream_zero` states that for any value `v` of type `K`, where `K` is a linear ordered field that also has a floor ring structure, the zeroth element in the sequence (or stream) of integer and fractional pairs of the generalised continued fraction of `v` is equal to the pair that's created with `v`'s integer and fractional part. In terms of mathematical notation, this means that for all `v` in `K` we have `GeneralizedContinuedFraction.IntFractPair.stream v 0 = some (GeneralizedContinuedFraction.IntFractPair.of v)`, where the function `stream` returns the sequence of integer and fractional parts and `IntFractPair.of v` returns a pair of `v`'s integer part and fractional part.
More concisely: For any element `v` in a linear ordered field `K` with floor ring structure, the zeroth element of the generalized continued fraction sequence of `v` is equal to the pair of `v`'s integer and fractional parts.
|
GeneralizedContinuedFraction.convergents'_succ
theorem GeneralizedContinuedFraction.convergents'_succ :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K) (n : ℕ),
(GeneralizedContinuedFraction.of v).convergents' (n + 1) =
↑⌊v⌋ + 1 / (GeneralizedContinuedFraction.of (Int.fract v)⁻¹).convergents' n
This theorem describes a recurrence relation for the `convergents'` (approximations of a real number) of the continued fraction expansion of an element `v` of a linear ordered field `K`. Specifically, the `n + 1`-th convergent of `v` is equal to the floor of `v` plus the reciprocal of the `n`-th convergent of the inverse of the fractional part of `v`. In other words, each convergent in the continued fraction expansion of `v` is computed based on the floor of `v` and the convergents of the inverse of `v`'s fractional part.
More concisely: The `(n+1)`-th convergent of a real number `v` in its continued fraction expansion is given by `floor v + 1 / (squared abs (v - floor v) + (n+1) * (reciprocal (fractionalPart v)))`, where `floor`, `squared abs`, `fractionalPart`, and `reciprocal` are defined in the linear ordered field `K`.
|
GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_some_iff
theorem GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_some_iff :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {n : ℕ}
{ifp_succ_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
∃ ifp_n,
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n ∧
ifp_n.fr ≠ 0 ∧ GeneralizedContinuedFraction.IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
This theorem provides a recurrence to calculate the `n + 1`th element in a sequence of integer and fractional parts of a value in the event of sequence non-termination. Specifically, for any linear ordered field `K`, floor ring `K`, value `v` of type `K`, natural number `n`, and `ifp_succ_n` which is the integer and fractional pair at the `n + 1`th position of the sequence of `v`, it states that `ifp_succ_n` is the `n + 1`th element of the sequence if and only if there exists some `ifp_n` such that `ifp_n` is the `n`th element of the sequence, the fractional part of `ifp_n` is not zero, and the pair created from the reciprocal of the fractional part of `ifp_n` is equal to `ifp_succ_n`.
More concisely: For any linear ordered field K, given a value v of type K and a natural number n, the integer and fractional pair at position n+1 in the sequence of v is the successor pair if and only if there exists the pair at position n with non-zero fractional part whose reciprocal gives the pair at position n+1.
|
GeneralizedContinuedFraction.IntFractPair.seq1_fst_eq_of
theorem GeneralizedContinuedFraction.IntFractPair.seq1_fst_eq_of :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K},
(GeneralizedContinuedFraction.IntFractPair.seq1 v).1 = GeneralizedContinuedFraction.IntFractPair.of v
The theorem `GeneralizedContinuedFraction.IntFractPair.seq1_fst_eq_of` states that for any type `K` which is a linear ordered field and also a floor ring, and for any value `v` of type `K`, the first element (or the head) of the sequence generated by `GeneralizedContinuedFraction.IntFractPair.seq1 v` is equal to the integer and fractional pair created from `v` using `GeneralizedContinuedFraction.IntFractPair.of v`. In other words, the head of the sequence is just the integer part of `v`.
More concisely: For any linear ordered field and floor ring `K` and `v` in `K`, the head of the sequence generated by `GeneralizedContinuedFraction.IntFractPair.seq1 v` equals the integer part of `v`.
|
GeneralizedContinuedFraction.convergents'_of_int
theorem GeneralizedContinuedFraction.convergents'_of_int :
∀ (K : Type u_1) [inst : LinearOrderedField K] [inst_1 : FloorRing K] (n : ℕ) (a : ℤ),
(GeneralizedContinuedFraction.of ↑a).convergents' n = ↑a
This theorem states that for any integer `a` and any natural number `n`, the `n`th convergent of the continued fraction expansion of `a` (designated as `GeneralizedContinuedFraction.of ↑a`) is always equal to `a`. Here, the type `K` is any linear ordered field that also has a floor ring structure. In simpler terms, it means that the approximations produced by taking the first `n` terms of the continued fraction expansion of an integer always give back the original integer.
More concisely: For any integer `a` and natural number `n`, the `n`th convergent of the continued fraction expansion of `a` equals `a`, in any linear ordered field `K` with a floor ring structure.
|
GeneralizedContinuedFraction.of_s_tail
theorem GeneralizedContinuedFraction.of_s_tail :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K),
(GeneralizedContinuedFraction.of v).s.tail = (GeneralizedContinuedFraction.of (Int.fract v)⁻¹).s
The theorem `GeneralizedContinuedFraction.of_s_tail` states that for any element `v` of a type `K` that forms a linear ordered field and has a floor ring structure, the tail of the coefficient sequence of the generalized continued fraction of `v` is equal to the coefficient sequence of the generalized continued fraction of the inverse of the fractional part of `v`. In other words, it relates the continued fraction expansion of a number with the continued fraction expansion of the inverse of its fractional part.
More concisely: Given a linear ordered field `K` element `v` with a floor ring structure, the tail of `v`'s generalized continued fraction coefficients is equal to the coefficients of the generalized continued fraction of `1/v.frac`.
|
GeneralizedContinuedFraction.IntFractPair.stream_succ_of_int
theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_of_int :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (a : ℤ) (n : ℕ),
GeneralizedContinuedFraction.IntFractPair.stream (↑a) (n + 1) = none
This theorem states that for any integer `a` and natural number `n`, the sequence of `IntFractPair`s (which represents the sequence of pairs of integer and fractional parts) associated with `a` stops after the first term. Here, `IntFractPair.stream (↑a)` creates the sequence from the integer `a`, and `(n + 1)` is the index of the term in the sequence. The theorem ensures that no term exists after the first one.
More concisely: For any integer `a`, the sequence of integer-fractional parts generated by `IntFractPair.stream (↑a)` is a singleton sequence, containing the pair `(a, 0)`.
|
GeneralizedContinuedFraction.IntFractPair.stream_succ_of_some
theorem GeneralizedContinuedFraction.IntFractPair.stream_succ_of_some :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {n : ℕ}
{p : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some p →
p.fr ≠ 0 →
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) =
some (GeneralizedContinuedFraction.IntFractPair.of p.fr⁻¹)
This theorem, `GeneralizedContinuedFraction.IntFractPair.stream_succ_of_some`, states that for any linear ordered field `K`, with floor ring structure, and any value `v` of type `K`, natural number `n`, and a pair `p` of an integer and the fractional part of a value, if the `n`-th element of the sequence (stream) generated by `v` is `p`, and the fractional part of `p` is not zero, then the `(n+1)`-th element of the sequence is the pair formed by taking the reciprocal of the fractional part of `p`. In essence, it provides a condition under which the next element in a generalized continued fraction sequence can be calculated from the current one.
More concisely: If in the generalized continued fraction sequence of a linear ordered field `K` with floor ring structure, the `n`-th element is the pair `(a, b)` such that `b` is the fractional part of some value `v` in `K` and `b ≠ 0`, then the `(n+1)`-th element is the pair `(a, 1/b)`.
|
GeneralizedContinuedFraction.get?_of_eq_some_of_succ_get?_intFractPair_stream
theorem GeneralizedContinuedFraction.get?_of_eq_some_of_succ_get?_intFractPair_stream :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {n : ℕ}
{ifp_succ_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) = some ifp_succ_n →
(GeneralizedContinuedFraction.of v).s.get? n = some { a := 1, b := ↑ifp_succ_n.b }
The theorem `GeneralizedContinuedFraction.get?_of_eq_some_of_succ_get?_intFractPair_stream` states that for any LinearOrderedField `K`, FloorRing `K`, value `v` of type `K`, and natural number `n`, if we have an integer-fraction pair `ifp_succ_n` such that the (n + 1)-th element of the stream of integer and fractional parts of `v` is `ifp_succ_n`, then the n-th entry of the sequence of the computed continued fraction of `v` is a pair whose first element is 1 and whose second element is the fractional part of `ifp_succ_n`.
More concisely: For any LinearOrderedField K, FloorRing K, value v of type K, and natural number n, if the (n+1)-th integer-fraction pair in the stream of the rational representation of v is (a, b) such that v = a + b/K.1, then the n-th entry in the continued fraction of v is (1, b).
|
GeneralizedContinuedFraction.of_h_eq_floor
theorem GeneralizedContinuedFraction.of_h_eq_floor :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K},
(GeneralizedContinuedFraction.of v).h = ↑⌊v⌋
This theorem states that for any type `K` that is a linear ordered field and has a floor ring structure, the head term of the generalized continued fraction representation of any value `v` of type `K` is equal to the integer part (or floor) of `v`. In mathematical terms, it asserts that the first term of the generalized continued fraction (gcf) of a number `v` is `⌊v⌋`.
More concisely: For any linear ordered field `K` with a floor ring structure, the first term of the generalized continued fraction representation of a value `v` in `K` equals the integer part of `v`.
|
GeneralizedContinuedFraction.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero
theorem GeneralizedContinuedFraction.get?_of_eq_some_of_get?_intFractPair_stream_fr_ne_zero :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {n : ℕ}
{ifp_n : GeneralizedContinuedFraction.IntFractPair K},
GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp_n →
ifp_n.fr ≠ 0 →
(GeneralizedContinuedFraction.of v).s.get? n =
some { a := 1, b := ↑(GeneralizedContinuedFraction.IntFractPair.of ifp_n.fr⁻¹).b }
This theorem states that for any type `K` that is a linear ordered field with a floor ring structure, and for any real number `v` and natural number `n`, if we have an integer-fraction pair `ifp_n` such that the `n`-th element of the stream of integer-fraction pairs of `v` is `ifp_n`, and if the fractional part of `ifp_n` is not zero, then the `n`-th element of the sequence of the generalized continued fraction of `v` is an object with the integer part being 1 and the fractional part being the integer part of the integer-fraction pair obtained from the reciprocal of the fractional part of `ifp_n`.
More concisely: For any linear ordered field `K` with a floor ring structure, if `v` is a real number in `K`, `n` is a natural number, and `ifp_n` is the `n`-th integer-fraction pair of `v` such that the fractional part of `ifp_n` is non-zero, then the `n`-th term of the generalized continued fraction of `v` is the integer-fraction pair with integer part 1 and fractional part being the integer part of the reciprocal of the fractional part of `ifp_n`.
|
GeneralizedContinuedFraction.IntFractPair.stream_succ
theorem GeneralizedContinuedFraction.IntFractPair.stream_succ :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K},
Int.fract v ≠ 0 →
∀ (n : ℕ),
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) =
GeneralizedContinuedFraction.IntFractPair.stream (Int.fract v)⁻¹ n
The theorem `GeneralizedContinuedFraction.IntFractPair.stream_succ` establishes a recurrence relation for the stream of `IntFractPair`s of a non-integer value `v`. Specifically, it states that for any non-integer `v`, provided that its fractional part is non-zero and for any natural number `n`, the `(n+1)`th term of the stream of `IntFractPair`s of `v` equals the `n`th term of the stream associated to the inverse of the fractional part of `v`. Here, `IntFractPair` is a pair consisting of an integer and the fractional part of a number, and the stream of `IntFractPair`s represents a sequence generated by some process.
More concisely: For any non-integer `v` with non-zero fractional part, the `(n+1)`th `IntFractPair` in the stream of `IntFractPair`s of `v` equals the `n`th `IntFractPair` in the stream of `IntFractPair`s of the inverse of `v`'s fractional part.
|
GeneralizedContinuedFraction.of_s_of_int
theorem GeneralizedContinuedFraction.of_s_of_int :
∀ (K : Type u_1) [inst : LinearOrderedField K] [inst_1 : FloorRing K] (a : ℤ),
(GeneralizedContinuedFraction.of ↑a).s = Stream'.Seq.nil
This theorem states that for any integer `a`, when we express `a` as a generalized continued fraction (a representation of a number as the sum of an integer and a reciprocal), the sequence of coefficients (`s`) in the fraction is empty. This is true for any `K` that is a type representing a linearly ordered field with a floor ring structure. The "floor ring" structure allows us to take the "floor" of elements from `K`, which is a crucial operation in the definition of continued fractions.
More concisely: For any integer `a` and any linearly ordered field `K` with a floor ring structure, the generalized continued fraction of `a` in `K` has an empty sequence of coefficients.
|
GeneralizedContinuedFraction.of_s_head
theorem GeneralizedContinuedFraction.of_s_head :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K},
Int.fract v ≠ 0 → (GeneralizedContinuedFraction.of v).s.head = some { a := 1, b := ↑⌊(Int.fract v)⁻¹⌋ }
This theorem relates to the generalized continued fraction representation of a non-integer number `v`. Specifically, it states that for any non-integer `v` where the fractional part of `v` is not zero, the first pair of coefficients of the continued fraction representation of `v` is given by `{a := 1, b := floor(1/fractional part of v)}`. This essentially expresses how the first term of the continued fraction (excluding the integral part) is constructed. In the context of number theory, continued fractions provide a way of representing real numbers that can reveal significant properties about them.
More concisely: For any non-integer `v` with non-zero fractional part, the first two coefficients of its generalized continued fraction representation are `(1, floor(1/v!.fr))`, where `v!` denotes the IEEE floating-point representation of `v`.
|
GeneralizedContinuedFraction.of_s_succ
theorem GeneralizedContinuedFraction.of_s_succ :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] (v : K) (n : ℕ),
(GeneralizedContinuedFraction.of v).s.get? (n + 1) = (GeneralizedContinuedFraction.of (Int.fract v)⁻¹).s.get? n
The theorem `GeneralizedContinuedFraction.of_s_succ` provides a recursive relation for the computation of the `n+1`th element of the sequence `s` that arises in the generalized continued fraction representation of a number `v` from a linearly ordered field `K`. Specifically, this `n+1`th element can be obtained from the `n`th element of the sequence `s` corresponding to the generalized continued fraction representation of the inverse of the fractional part of `v`. Here, `Int.fract v` stands for the fractional part of `v`, which is the result of subtracting the floor of `v` from `v` itself.
More concisely: The `(n+1)`th element of the generalized continued fraction representation of a number `v` from a linearly ordered field `K` is given recursively by the `n`th element of the sequence for the inverse of `v`'s fractional part.
|
GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_none_iff
theorem GeneralizedContinuedFraction.IntFractPair.succ_nth_stream_eq_none_iff :
∀ {K : Type u_1} [inst : LinearOrderedField K] [inst_1 : FloorRing K] {v : K} {n : ℕ},
GeneralizedContinuedFraction.IntFractPair.stream v (n + 1) = none ↔
GeneralizedContinuedFraction.IntFractPair.stream v n = none ∨
∃ ifp, GeneralizedContinuedFraction.IntFractPair.stream v n = some ifp ∧ ifp.fr = 0
This theorem describes a condition for the termination of a sequence of integer and fractional parts of a value in a generalized continued fraction. Specifically, for any linear ordered field `K` with a floor ring structure, and any value `v` of type `K` and natural number `n`, the `n+1`th element of the sequence is `none` (indicating termination) if and only if the `n`th element is `none` or there exists an integer-fraction pair `ifp` such that the `n`th element of the sequence is `ifp` and the fractional part of `ifp` is zero.
More concisely: For any linear ordered field `K` with a floor ring structure and value `v` in `K`, the generalized continued fraction of `v` terminates if and only if the `n`th term is `none` or equals an integer-fraction pair `(i, r)` with `r = 0`.
|