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

Summary

We show that the generalized_continued_fraction given by GeneralizedContinuedFraction.of in fact is a (regular) continued fraction. Using the equivalence of the convergents computations (GeneralizedContinuedFraction.convergents and GeneralizedContinuedFraction.convergents') for continued fractions (see Algebra.ContinuedFractions.ConvergentsEquiv), it follows that the convergents computations for GeneralizedContinuedFraction.of are equivalent.

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

Main Definitions

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

Main Theorems

• GeneralizedContinuedFraction.of_convergents_eq_convergents' shows that the convergents computations for GeneralizedContinuedFraction.of are equivalent.
• GeneralizedContinuedFraction.of_convergence shows that (GeneralizedContinuedFraction.of v).convergents converges to v.

Tags

convergence, fractions

theorem GeneralizedContinuedFraction.of_isSimpleContinuedFraction {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : GeneralizedContinuedFraction.IsSimpleContinuedFraction (GeneralizedContinuedFraction.of v)

def SimpleContinuedFraction.of {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : SimpleContinuedFraction K

Creates the simple continued fraction of a value.

Equations

• SimpleContinuedFraction.of v = { val := GeneralizedContinuedFraction.of v, property := (_ : GeneralizedContinuedFraction.IsSimpleContinuedFraction (GeneralizedContinuedFraction.of v)) }

theorem SimpleContinuedFraction.of_isContinuedFraction {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : SimpleContinuedFraction.IsContinuedFraction (SimpleContinuedFraction.of v)

def ContinuedFraction.of {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : ContinuedFraction K

Creates the continued fraction of a value.

Equations

• ContinuedFraction.of v = { val := SimpleContinuedFraction.of v, property := (_ : SimpleContinuedFraction.IsContinuedFraction (SimpleContinuedFraction.of v)) }

theorem GeneralizedContinuedFraction.of_convergents_eq_convergents' {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] : GeneralizedContinuedFraction.convergents (GeneralizedContinuedFraction.of v) = GeneralizedContinuedFraction.convergents' (GeneralizedContinuedFraction.of v)

theorem GeneralizedContinuedFraction.convergents_succ {K : Type u_1} (v : K) [LinearOrderedField K] [FloorRing K] (n : ℕ) : GeneralizedContinuedFraction.convergents (GeneralizedContinuedFraction.of v) (n + 1) = ↑⌊v⌋ + 1 / GeneralizedContinuedFraction.convergents (GeneralizedContinuedFraction.of (Int.fract v)⁻¹) 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 (GeneralizedContinuedFraction.of v).convergents v converges to v.

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

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