mathlib3 documentation

algebra.continued_fractions.computation.approximation_corollaries

Corollaries From Approximation Lemmas (algebra.continued_fractions.computation.approximations) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Summary #

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

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

Main Definitions #

Main Theorems #

Tags #

convergence, fractions

source
theorem generalized_continued_fraction.of_is_simple_continued_fraction {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] :
(generalized_continued_fraction.of v).is_simple_continued_fraction
source
def simple_continued_fraction.of {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] :
simple_continued_fraction K

Creates the simple continued fraction of a value.

Equations
source
theorem simple_continued_fraction.of_is_continued_fraction {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] :
(simple_continued_fraction.of v).is_continued_fraction
source
def continued_fraction.of {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] :
continued_fraction K

Creates the continued fraction of a value.

Equations
source
theorem generalized_continued_fraction.of_convergents_eq_convergents' {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] :
(generalized_continued_fraction.of v).convergents = (generalized_continued_fraction.of v).convergents'
source
theorem generalized_continued_fraction.convergents_succ {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] (n : ℕ) :
(generalized_continued_fraction.of v).convergents (n + 1) = ↑⌊v⌋ + 1 / (generalized_continued_fraction.of (int.fract v)⁻¹).convergents 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 (generalized_continued_fraction.of v).convergents v converges to v.

source
theorem generalized_continued_fraction.of_convergence_epsilon {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] [archimedean K] (ε : K) (H : ε > 0) :
∃ (N : ℕ), ∀ (n : ℕ), n ≥ N → |v - (generalized_continued_fraction.of v).convergents n| < ε
source
theorem generalized_continued_fraction.of_convergence {K : Type u_1} (v : K) [linear_ordered_field K] [floor_ring K] [archimedean K] [order_topology K] :
filter.tendsto (generalized_continued_fraction.of v).convergents filter.at_top (nhds v)