Corollaries From Approximation Lemmas (Algebra.ContinuedFractions.Computation.Approximations)

Summary

Using the equivalence of the convergents computations (GenContFract.convs and GenContFract.convs') for continued fractions (see Algebra.ContinuedFractions.ConvergentsEquiv), it follows that the convergents computations for GenContFract.of are equivalent.

Moreover, we show the convergence of the continued fractions computations, that is (GenContFract.of v).convs indeed computes v in the limit.

Main Definitions

• ContFract.of returns the (regular) continued fraction of a value.

Main Theorems

• GenContFract.of_convs_eq_convs' shows that the convergents computations for GenContFract.of are equivalent.
• GenContFract.of_convergence shows that (GenContFract.of v).convs converges to v.

Tags

convergence, fractions

theorem GenContFract.of_convs_eq_convs' {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : (GenContFract.of v).convs = (GenContFract.of v).convs'

theorem GenContFract.convs_succ {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] (n : ℕ) : (GenContFract.of v).convs (n + 1) = ↑⌊v⌋ + 1 / (GenContFract.of (Int.fract v)⁻¹).convs n

The recurrence relation for the convergents of the continued fraction expansion of an element v of K in terms of the convergents of the inverse of its fractional part.

Convergence

We next show that (GenContFract.of v).convs v converges to v.

theorem GenContFract.of_convergence_epsilon {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] [Archimedean K] (ε : K) : ε > 0 → ∃ (N : ℕ), ∀ n ≥ N, |v - (GenContFract.of v).convs n| < ε

theorem GenContFract.of_convergence {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] [Archimedean K] [TopologicalSpace K] [OrderTopology K] : Filter.Tendsto (GenContFract.of v).convs Filter.atTop (nhds v)