Periodic continued fractions

DefinitionEventually periodic continued fractions#✓fully proved

Let \(x\) be a real number with regular continued fraction \([a_0; a_1, a_2, \dots]\). The continued fraction of \(x\) is eventually periodic if it does not terminate and its sequence of partial denominators \((a_n)_{n \ge 1}\), which omits the head coefficient \(a_0\), is eventually periodic: there are natural numbers \(p > 0\) and \(n_0 \ge 1\) such that \(a_{n+p} = a_n\) for every \(n \ge n_0\).

def ContinuedFractionEventuallyPeriodic (x : ℝ) : Prop :=
  ¬ (GenContFract.of x).Terminates ∧
    IsEventuallyPeriodic (fun n => (GenContFract.of x).partDens.get? n)

Sources

• Nimbran–Levrie lines 130–134.

Uses 1 · Used by 3

Statement usesEventually periodic sequences

Used byEuler–Lagrange theorem · Lagrange's theorem on periodic continued fractions · Euler's theorem on periodic continued fractions

DefinitionReal quadratic irrationals#✓fully proved

A real number \(x\) is a real quadratic irrational if it is integral (equivalently, algebraic) over \(\mathbb{Q}\) and its minimal polynomial over \(\mathbb{Q}\) has degree \(2\).

Degree two over \(\mathbb{Q}\) captures real quadratic irrationality: such \(x\) is exactly an irrational root of a quadratic polynomial with rational coefficients.

def IsRealQuadraticIrrational (x : ℝ) : Prop :=
  IsIntegral ℚ x ∧ (minpoly ℚ x).natDegree = 2

Sources

• Nimbran–Levrie line 136 (Euler–Lagrange statement).

Used by 4

Used byLagrange's theorem for Mallows representations · Euler–Lagrange theorem · Lagrange's theorem on periodic continued fractions · Euler's theorem on periodic continued fractions

TheoremLagrange's theorem on periodic continued fractions#✓fully proved

If a real number \(x\) is a real quadratic irrational, then the continued fraction of \(x\) is eventually periodic.

theorem continuedFractionEventuallyPeriodic_of_isRealQuadraticIrrational
    (x : ℝ) (h : IsRealQuadraticIrrational x) :
    ContinuedFractionEventuallyPeriodic x

Uses 5 · Used by 1

Statement usesEventually periodic continued fractions · Real quadratic irrationals

Proof usesEventually periodic sequences · Orbits in a finite set are eventually periodic · Explicit period and preperiod give eventual periodicity

Used byEuler–Lagrange theorem

TheoremEuler's theorem on periodic continued fractions#✓fully proved

If the continued fraction of a real number \(x\) is eventually periodic, then \(x\) is a real quadratic irrational.

theorem isRealQuadraticIrrational_of_continuedFractionEventuallyPeriodic
    (x : ℝ) (h : ContinuedFractionEventuallyPeriodic x) :
    IsRealQuadraticIrrational x

Uses 3 · Used by 1

Statement usesEventually periodic continued fractions · Real quadratic irrationals

Proof usesEventually periodic sequences

Used byEuler–Lagrange theorem

TheoremEuler–Lagrange theorem#✓fully proved

A real number \(x\) has an eventually periodic continued fraction if and only if \(x\) is a real quadratic irrational.

The theorem asserts neither pure periodicity nor the stronger criterion for reduced quadratic irrationals.

theorem continuedFractionEventuallyPeriodic_iff_isRealQuadraticIrrational
    (x : ℝ) : ContinuedFractionEventuallyPeriodic x ↔ IsRealQuadraticIrrational x

Sources

• Nimbran–Levrie line 136.

Uses 4

Statement usesEventually periodic continued fractions · Real quadratic irrationals

Proof usesLagrange's theorem on periodic continued fractions · Euler's theorem on periodic continued fractions

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.