Second-order recurrences from seed triples

DefinitionCoefficient of the formal-sequence recurrence#✓fully proved

For elements \(a\), \(b\), \(c\) of a field \(F\), the coefficient of the formal-sequence recurrence determined by the seed triplet \((a, b, c)\) is \(\alpha = \frac{ab + bc + ca}{b^2} - 1\).

Division by zero is read as \(0\), so \(\alpha = -1\) when \(b = 0\).

public def formalAlpha {F : Type*} [Field F] (a b c : F) : F :=
  (a * b + b * c + c * a) / b ^ 2 - 1
Sources
Used by 1
Used byFormal sequence from a seed triplet

DefinitionConstant term of the formal-sequence recurrence#✓fully proved

For elements \(a\), \(b\), \(c\) of a field \(F\), the constant term of the formal-sequence recurrence determined by the seed triplet \((a, b, c)\) is \(\beta = \frac{b^2 - ac}{b}\).

Division by zero is read as \(0\), so \(\beta = 0\) when \(b = 0\).

public def formalBeta {F : Type*} [Field F] (a b c : F) : F :=
  (b ^ 2 - a * c) / b
Sources
Used by 1
Used byFormal sequence from a seed triplet

DefinitionFormal sequence from a seed triplet#✓fully proved

Let \(F\) be a field and \(a, b, c \in F\). A sequence \(u : \mathbb{N} \to F\) is a formal sequence with seed triplet \((a, b, c)\) when \(b \neq 0\), \(u_0 = a\), \(u_1 = b\), \(u_2 = c\), and for every \(n \ge 0\)

\[u_{n+2} = \alpha u_{n+1} - u_n + \beta,\]

where \(\alpha = \frac{ab + bc + ca}{b^2} - 1\) and \(\beta = \frac{b^2 - ac}{b}\) are the coefficient and the constant term of the formal-sequence recurrence.

public def IsFormalSequence {F : Type*} [Field F]
    (u : ℕ → F) (a b c : F) : Prop :=
  b ≠ 0 ∧ u 0 = a ∧ u 1 = b ∧ u 2 = c ∧
    ∀ n : ℕ, u (n + 2) =
      formalAlpha a b c * u (n + 1) - u n + formalBeta a b c
Sources
Uses 2
Statement usesCoefficient of the formal-sequence recurrence · Constant term of the formal-sequence recurrence
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.