Pell and Pell–Lucas numbers

DefinitionPell–Lucas numbers#✓fully proved

The Pell–Lucas numbers are the natural numbers \(Q_n\) defined by \(Q_0 = Q_1 = 2\) and \(Q_{n+2} = 2 Q_{n+1} + Q_n\) for every natural number \(n\).

They are the specialization \(L_{1,n}(2,1)\) of the generalized bivariate Lucas \(p\)-polynomials \(L_{p,n}(x,y)\) of Kaygisiz and Şahin.

public def pellLucas : Nat → Nat
  | 0 => 2
  | 1 => 2
  | n + 2 => 2 * pellLucas (n + 1) + pellLucas n
Used by 3
Used byThe \(2\)-generalized Pell–Lucas numbers are the Pell–Lucas numbers · Toeplitz–Hessenberg determinants with Oresme entries · Pell and Pell–Lucas numbers as composition sums with \(\sqrt 2\) weights

TheoremCassini's identity for Pell numbers#✓fully proved

Let \((P_n)_{n \ge 0}\) be the Pell numbers, the natural numbers with \(P_0 = 0\), \(P_1 = 1\) and \(P_{n+2} = 2P_{n+1} + P_n\) for every \(n \ge 0\). Then for every natural number \(k \ge 1\),

\[ P_{k-1} P_{k+1} = P_k^2 + (-1)^k. \]
theorem pell_cassini_identity
    (P : ℕ → ℕ)
    (hP_zero : P 0 = 0)
    (hP_one : P 1 = 1)
    (hP_step : ∀ n : ℕ, P (n + 2) = 2 * P (n + 1) + P n)
    (k : ℕ)
    (hk : 1 ≤ k) :
    (P (k - 1) : ℤ) * (P (k + 1) : ℤ) =
      (P k : ℤ) ^ 2 + (-1 : ℤ) ^ k
Sources
  • aBa Mbirika, Janee Schrader, and Jürgen Spilker, "Pell and Associated Pell Braid Sequences as GCDs of Sums of k Consecutive Pell, Balancing, and Related Numbers," Journal of Integer Sequences 26 (2023), Article 23.6.4, Lemma, lines 367–369, https://cs.uwaterloo.ca/journals/JIS/VOL26/Mbirika/mbir5.tex; attributed there to Horadam, Identity (30).

DefinitionPell–Lucas sequence#✓fully proved

The Pell–Lucas (associated Pell) numbers \(Q_n\), for natural numbers \(n\), are defined by \(Q_0 = 1\), \(Q_1 = 1\) and \(Q_{n+2} = 2Q_{n+1} + Q_n\) for every \(n\). They begin \(1, 1, 3, 7, 17, \dots\) (OEIS A001333).

def pellLucasSequence : ℕ → ℕ
  | 0 => 1
  | 1 => 1
  | n + 2 => 2 * pellLucasSequence (n + 1) + pellLucasSequence n
Sources
Used by 13
Used byNumeration by Pell and half-companion Pell numbers · Numeration by doubled Pell and half-companion Pell numbers · Floor of greedy Pell sums times \(1 + \sqrt 2\) · Floor of greedy sums of \(2P_k\) and \(H_k\) times \((2 + \sqrt 2)/2\) · Odd Pell and even Pell–Lucas numbers times \(1 + \sqrt 2\) · P-positions of the silver game · Consecutive Pell–Lucas numbers are coprime · Pell and Pell–Lucas numbers are coprime · Square Pell–Lucas numbers · Sums of powers of consecutive Pell–Lucas numbers that are squares · Pell–Lucas–Oresme convolution · Oresme–Pell–Lucas congruence modulo 49 · Recurrence for the Pell–Lucas numbers

TheoremRecurrence for the Pell–Lucas numbers#✓fully proved

Write \(Q_n\) for the \(n\)-th Pell–Lucas (associated Pell) number. For every natural number \(n\), \(Q_{n+2} = 2Q_{n+1} + Q_n\).

theorem pellLucasSequence_succ_succ (n : ℕ) :
    pellLucasSequence (n + 2) =
      2 * pellLucasSequence (n + 1) + pellLucasSequence n
Uses 1
Statement usesPell–Lucas sequence

DefinitionPell numbers#✓fully proved

The Pell numbers \(P_n\), for natural numbers \(n\), are defined by \(P_0 = 0\), \(P_1 = 1\) and \(P_{n+2} = 2P_{n+1} + P_n\) for every \(n\). They begin \(0, 1, 2, 5, 12, \dots\)

def pellNumber : ℕ → ℕ
  | 0 => 0
  | 1 => 1
  | n + 2 => 2 * pellNumber (n + 1) + pellNumber n
Sources
Used by 21
Used bySellers' domino tiling theorem, recursive Pell form · Sellers' domino tiling theorem · Numeration by Pell and half-companion Pell numbers · Numeration by doubled Pell and half-companion Pell numbers · Floor of greedy Pell sums times \(1 + \sqrt 2\) · Floor of greedy sums of \(2P_k\) and \(H_k\) times \((2 + \sqrt 2)/2\) · Odd Pell and even Pell–Lucas numbers times \(1 + \sqrt 2\) · P-positions of the silver game · Pell and Pell–Lucas numbers are coprime · Triple convolution of Pell numbers with two consecutive Fibonacci step sequences · Pell–Fibonacci–tribonacci triple sum via a Pell–tribonacci convolution · Convolution of the Pell numbers with the Fibonacci numbers · Closed form for the Pell–Fibonacci–tribonacci triple convolution · Power-weighted Pell sums along odd multiples · Pell–Oresme convolution · Oresme–Pell congruence modulo 49 · Composition-sum formulas for \(F_{n+3}\), \(F_{3n+1}\) and Jacobsthal and Pell numbers · Composition-sum formulas for \(F_{2n}\), \(F_{3n-1}\) and \(P_{n-1}\) · Toeplitz–Hessenberg determinants with Oresme entries · Pell and Pell–Lucas numbers as composition sums with \(\sqrt 2\) weights · Sum-of-cubes identities for Fibonacci, Pell, Jacobsthal and Mersenne numbers

TheoremBinomial transform of the Pell numbers#✓fully proved

Let \(P \colon \mathbb{N} \to \mathbb{Z}\) satisfy \(P_0 = 0\), \(P_1 = 1\) and \(P_{n+2} = 2 P_{n+1} + P_n\) for every \(n\), so that \(P_n\) is the \(n\)-th Pell number. Then for every natural number \(n\),

\[\sum_{i=0}^{n} \binom{n}{i} P_i = \sum_{k=0}^{n} \left(\frac{k}{8}\right) \binom{2n}{n+k},\]

where \(\left(\frac{k}{8}\right)\) is the Kronecker symbol: it is \(0\) for even \(k\), \(1\) for \(k \equiv \pm 1 \pmod 8\) and \(-1\) for \(k \equiv \pm 3 \pmod 8\).

Both sides give \(0, 1, 4, 14, 48, 164, \dots\) (OEIS A007070) for \(n = 0, \dots, 5\).

theorem pell_binomial_transform
    (P : ℕ → ℤ) (h0 : P 0 = 0) (h1 : P 1 = 1)
    (hrec : ∀ n, P (n + 2) = 2 * P (n + 1) + P n) (n : ℕ) :
    ∑ i ∈ Finset.range (n + 1), (n.choose i : ℤ) * P i =
    ∑ k ∈ Finset.range (n + 1),
      (if k % 2 = 0 then (0 : ℤ) else if k % 8 = 1 ∨ k % 8 = 7 then 1 else -1) *
      ((2 * n).choose (n + k) : ℤ)
Sources
  • Greg Dresden and Yike Li, "Periodic Weighted Sums of Binomial Coefficients," Journal of Integer Sequences 26 (2023), Article 23.8.7, Corollary (equation e.12), lines 369–379, https://cs.uwaterloo.ca/journals/JIS/VOL26/Dresden/dresden26.tex
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.