Abstract
This article provides a formalisation of continued fractions of real numbers and their basic properties.
It also contains a proof of the classic result that the irrational numbers with periodic continued
fraction expansions are precisely the quadratic irrationals, i.e. real numbers that fulfil a non-trivial quadratic equation
Particular attention is given to the continued fraction expansion of
This is then also used to provide a fairly efficient, executable, and fully formalised algorithm to
compute solutions to Pell's equation
Lastly, a derivation of the continued fraction expansions of Euler's number
License
Topics
Session Continued_Fractions
- Continued_Fractions
- Quadratic_Irrationals
- E_CFrac
- Sqrt_Nat_Cfrac
- Pell_Lifting
- Pell_Continued_Fraction
- Pell_Continued_Fraction_Tests
- Continued_Fraction_Approximation