Normal second-order sequences

DefinitionNormal second-order number sequence#✓fully proved

For integers \(a_1\) and \(a_2\), the normal second-order number sequence \((u_n)_{n \ge 0}\) with coefficients \(a_1, a_2\) is the integer sequence defined by \(u_0 = 0\), \(u_1 = 1\) and \(u_{n+2} = a_1 u_{n+1} + a_2 u_n\) for every \(n \ge 0\).

The source requires \(a_1\) and \(a_2\) to be nonzero and starts the sequence at \(u_1\); the value \(u_0 = 0\) extends it, and the indices \(u_1, u_2, \dots\) agree with the source.

def normalSeq (a1 a2 : ℤ) : ℕ → ℤ
  | 0 => 0
  | 1 => 1
  | (n + 2) => a1 * normalSeq a1 a2 (n + 1) + a2 * normalSeq a1 a2 n

Used by 5

Used byNormal number sequence with second coefficient one · Addition formula for the normal sequence with second coefficient one · First term of a normal number sequence · Recurrence for a normal number sequence · Second term of a normal number sequence

TheoremFirst term of a normal number sequence#✓fully proved

For all integers \(a_1\) and \(a_2\), the normal second-order number sequence \((u_n)_{n \ge 0}\) with coefficients \(a_1, a_2\) has \(u_1 = 1\).

theorem normalSeq_one (a1 a2 : ℤ) :
    normalSeq a1 a2 1 = 1

Uses 1

Statement usesNormal second-order number sequence

TheoremSecond term of a normal number sequence#✓fully proved

For all integers \(a_1\) and \(a_2\), the normal second-order number sequence \((u_n)_{n \ge 0}\) with coefficients \(a_1, a_2\) has \(u_2 = a_1\).

theorem normalSeq_two (a1 a2 : ℤ) :
    normalSeq a1 a2 2 = a1

Uses 1

Statement usesNormal second-order number sequence

TheoremRecurrence for a normal number sequence#✓fully proved

For all integers \(a_1\) and \(a_2\) and every natural number \(n\), the normal second-order number sequence \((u_n)_{n \ge 0}\) with coefficients \(a_1, a_2\) satisfies \(u_{n+2} = a_1 u_{n+1} + a_2 u_n\).

theorem normalSeq_recurrence (a1 a2 : ℤ) (n : ℕ) :
    normalSeq a1 a2 (n + 2) =
      a1 * normalSeq a1 a2 (n + 1) + a2 * normalSeq a1 a2 n

Uses 1

Statement usesNormal second-order number sequence

DefinitionNormal number sequence with second coefficient one#✓fully proved

For an integer \(a\), this sequence is the normal second-order number sequence \((u_n)_{n \ge 0}\) with coefficients \(a_1 = a\) and \(a_2 = 1\); that is, \(u_0 = 0\), \(u_1 = 1\) and \(u_{n+2} = a u_{n+1} + u_n\) for every \(n \ge 0\).

The source takes \(a\) to be a nonzero integer; the definition allows every integer \(a\).

def normalSeqFib (a : ℤ) : ℕ → ℤ :=
  fun n => normalSeq a 1 n

Uses 1 · Used by 2

Statement usesNormal second-order number sequence

Used byAddition formula for the normal sequence with second coefficient one · Odd-index sum of two squares for the normal sequence with second coefficient one

TheoremAddition formula for the normal sequence with second coefficient one#✓fully proved

Let \(a\) be an integer and let \((u_n)_{n \ge 0}\) be the normal second-order number sequence with coefficients \(a_1 = a\) and \(a_2 = 1\). Then \(u_{m+n+1} = u_{m+1} u_{n+1} + u_m u_n\) for all natural numbers \(m\) and \(n\).

theorem normalSeqFib_add (a : ℤ) (m n : ℕ) :
    normalSeqFib a (m + n + 1) =
      normalSeqFib a (m + 1) * normalSeqFib a (n + 1) +
        normalSeqFib a m * normalSeqFib a n

Uses 2 · Used by 1

Statement usesNormal number sequence with second coefficient one

Proof usesNormal second-order number sequence

Used byOdd-index sum of two squares for the normal sequence with second coefficient one

TheoremOdd-index sum of two squares for the normal sequence with second coefficient one#✓fully proved

Let \(a\) be an integer and let \((u_n)_{n \ge 0}\) be the normal second-order number sequence with coefficients \(a_1 = a\) and \(a_2 = 1\). Then \(u_{2n-1} = u_n^2 + u_{n-1}^2\) for every natural number \(n \ge 2\).

The source assumes \(a \ne 0\); the identity holds for every integer \(a\).

theorem normalSeq_odd_identity (a : ℤ) (n : ℕ) (hn : 2 ≤ n) :
    normalSeqFib a (2 * n - 1) =
      (normalSeqFib a n) ^ 2 + (normalSeqFib a (n - 1)) ^ 2

Uses 2

Statement usesNormal number sequence with second coefficient one

Proof usesAddition formula for the normal sequence with second coefficient one

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.