Part 1 of 2

• Continued fractions of alternating series
• Continued fractions of Laurent series
• Continued fractions of quadratic irrationals
• Engel expansions
• Extended continuants and bi-infinite continued fractions
• Farey fractions with a given numerator
• Farey sequences
• Farey staircase
• Folding lemma and paperfolding continued fractions
• Gauss–Kuzmin masses of continued fraction strings
• Gauss–Kuzmin–Wirsing operator
• Hata's Farey formula for Euler's constant
• Lüroth series
• Periodic continued fractions
• Mallows representation of irrational numbers
• Pierce expansions
• Polynomial continued fractions and Farey paths
• TRIP-Stern sequences

DefinitionLaplace Q-polynomial families#✓fully proved

Let \(R\) be a semiring and let \((P_k)_{k \ge 0}\) and \((Q_k)_{k \ge 0}\) be sequences of polynomials in \(R[X]\). The sequence \((Q_k)\) is a Laplace Q-polynomial family companion to \((P_k)\) when \(Q_0 = 1\) and, for every natural number \(k \ge 1\),

\[Q_k = P_k + Q_{k-1}' \quad \text{and} \quad Q_{k+1} = X Q_k + (k + 1) Q_{k-1},\]

where \(Q_{k-1}'\) denotes the formal derivative of \(Q_{k-1}\).

public def IsLaplaceQFamily (P Q : ℕ → Polynomial R) : Prop :=
  Q 0 = 1 ∧
    ∀ k : ℕ, 1 ≤ k →
      Q k = P k + Polynomial.derivative (Q (k - 1)) ∧
        Q (k + 1) = Polynomial.X * Q k + (k + 1) • Q (k - 1)

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL19/Kreinin/kreinin4.tex, lines 306-315.

TheoremSolutions of \(P u^2 + Q u y + R y^2 = 1\) give convergents of \(-Q/(2P)\)#✓fully proved

Let \(P, Q, R, u, y\) be integers with \(P > 0\) and \(y > 0\), and let \(D = Q^2 - 4PR\). Assume that \(D < 0\), that \(D \ne -3\), and that \(P \ne 2\) if \(D = -4\). If \(P u^2 + Q u y + R y^2 = 1\), then, writing \(\omega = -Q/(2P)\) with regular continued fraction expansion \(\omega = [a_0; a_1, a_2, \dots]\), there is a natural number \(n\) such that \(u/y\) equals the \(n\)-th convergent of \(\omega\) and either \(n = 0\) or the partial quotient \(a_n\) exists (the expansion has not terminated before \(a_n\)).

A solution of \(P u^2 + Q u y + R y^2 = 1\) automatically has \(\gcd(u, y) = 1\), as the source's lemma requires; the exclusion \(D \ne -3\) and the condition that \(D = -4\) implies \(P \ne 2\) are exactly the source theorem's.

Proof: Following Matthews' theorem and lemma, complete the square, establish the Legendre approximation bound, and choose the least convergent index so that termination cannot have occurred earlier.

public theorem lagrange_quadratic_convergent
    (P Q R u y : ℤ) (hP : 0 < P) (hy : 0 < y)
    (hD : Q ^ 2 - 4 * P * R < 0)
    (hD3 : Q ^ 2 - 4 * P * R ≠ -3)
    (hD4 : Q ^ 2 - 4 * P * R = -4 → P ≠ 2)
    (hsol : P * u ^ 2 + Q * u * y + R * y ^ 2 = 1) :
    let ω : ℝ := -(Q : ℝ) / (2 * (P : ℝ))
    ∃ n : ℕ,
      (n = 0 ∨ ¬(GenContFract.of ω).TerminatedAt (n - 1)) ∧
        ((ω.convergent n : ℚ) : ℝ) = (u : ℝ) / (y : ℝ)

Sources

• Keith R. Matthews, "Lagrange's Algorithm Revisited: Solving at^2 + btu + cu^2 = n in the Case of Negative Discriminant," Journal of Integer Sequences 17 (2014), Article 14.11.1, Theorem, lines 167–169, equation, lines 109–111, Lemma, lines 120–122, https://cs.uwaterloo.ca/journals/JIS/VOL17/Matthews/matt10.tex

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.