k-generalized Lucas numbers

Definition\(k\)-generalized Lucas numbers#✓fully proved

For a natural number \(k \ge 2\), the \(k\)-generalized Lucas numbers \(L^{(k)}_n\) are the natural numbers indexed by the integers \(n \ge 2 - k\) given by \(L^{(k)}_n = 0\) for \(2 - k \le n \le -1\), \(L^{(k)}_0 = 2\), \(L^{(k)}_1 = 1\), and \(L^{(k)}_n = L^{(k)}_{n-1} + L^{(k)}_{n-2} + \dots + L^{(k)}_{n-k}\) for every integer \(n \ge 2\). No value is assigned at indices below \(2 - k\).

public def kGeneralizedLucas (k : ℕ) (_hk : 2 ≤ k) (n : ℤ)
    (_h : 2 - (k : ℤ) ≤ n) : ℕ :=
  (⟨k, fun _ => 1⟩ : LinearRecurrence ℕ).mkSol
    (fun i : Fin k => if i.val + 2 = k then 2 else if i.val + 1 = k then 1 else 0)
    ((n - (2 - (k : ℤ))).toNat)
Used by 5
Used by\(k\)-generalized Lucas numbers at the lowest index · \(k\)-generalized Lucas numbers vanish at negative indices · \(k\)-generalized Lucas numbers at index one · Recurrence for the \(k\)-generalized Lucas numbers · \(k\)-generalized Lucas numbers at index zero

Theorem\(k\)-generalized Lucas numbers at index zero#✓fully proved

For every natural number \(k \ge 2\), the \(k\)-generalized Lucas number \(L^{(k)}_0\) equals \(2\).

public theorem kGeneralizedLucas_zero (k : ℕ) (hk : 2 ≤ k)
    (h0 : 2 - (k : ℤ) ≤ 0) :
    kGeneralizedLucas k hk 0 h0 = 2
Uses 1
Statement uses\(k\)-generalized Lucas numbers

Theorem\(k\)-generalized Lucas numbers at index one#✓fully proved

For every natural number \(k \ge 2\), the \(k\)-generalized Lucas number \(L^{(k)}_1\) equals \(1\).

public theorem kGeneralizedLucas_one (k : ℕ) (hk : 2 ≤ k)
    (h1 : 2 - (k : ℤ) ≤ 1) :
    kGeneralizedLucas k hk 1 h1 = 1
Uses 1
Statement uses\(k\)-generalized Lucas numbers

Theorem\(k\)-generalized Lucas numbers vanish at negative indices#✓fully proved

For every natural number \(k \ge 3\) and every integer \(n\) with \(2 - k \le n \le -1\), the \(k\)-generalized Lucas number \(L^{(k)}_n\) equals \(0\).

public theorem kGeneralizedLucas_neg_eq_zero (k : ℕ) (hk : 3 ≤ k) (n : ℤ)
    (h : 2 - (k : ℤ) ≤ n) (hn : n ≤ -1) :
    kGeneralizedLucas k (Nat.le_trans (by decide : 2 ≤ 3) hk) n h = 0
Uses 1 · Used by 1
Statement uses\(k\)-generalized Lucas numbers
Used by\(k\)-generalized Lucas numbers at the lowest index

Theorem\(k\)-generalized Lucas numbers at the lowest index#✓fully proved

For every natural number \(k \ge 3\), the \(k\)-generalized Lucas number \(L^{(k)}_{2-k}\) equals \(0\).

public theorem kGeneralizedLucas_lower_zero (k : ℕ) (hk : 3 ≤ k)
    (h : 2 - (k : ℤ) ≤ 2 - (k : ℤ)) :
    kGeneralizedLucas k (Nat.le_trans (by decide : 2 ≤ 3) hk) (2 - (k : ℤ)) h =
      0
Uses 2
Statement uses\(k\)-generalized Lucas numbers
Proof uses\(k\)-generalized Lucas numbers vanish at negative indices

TheoremRecurrence for the \(k\)-generalized Lucas numbers#✓fully proved

For every natural number \(k \ge 2\) and every integer \(n \ge 2\), the \(k\)-generalized Lucas numbers satisfy \(L^{(k)}_n = \sum_{i=0}^{k-1} L^{(k)}_{n-k+i}\), that is, \(L^{(k)}_n\) is the sum \(L^{(k)}_{n-1} + \dots + L^{(k)}_{n-k}\) of the \(k\) preceding values.

public theorem kGeneralizedLucas_recurrence (k : ℕ) (hk : 2 ≤ k) (n : ℤ)
    (hn : 2 ≤ n) (h : 2 - (k : ℤ) ≤ n) :
    kGeneralizedLucas k hk n h =
      ∑ i : Fin k,
        kGeneralizedLucas k hk ((n - (k : ℤ)) + (i.val : ℤ)) (by omega)
Uses 1
Statement uses\(k\)-generalized Lucas numbers

DefinitionFinite prefixes of the n-step Lucas numbers#✓fully proved

For natural numbers \(n\) and \(m\), this is the list \([L^{(n)}_1, \dots, L^{(n)}_m]\) of length \(m\) (empty for \(m = 0\)), where \(L^{(n)}_k = 2^k - 1\) for \(1 \le k \le n\) and \(L^{(n)}_k\) is the sum of the \(n\) preceding terms for \(k \ge n + 1\). For \(n = 0\) every term is \(0\).

def nStepLucasList (n : ℕ) : ℕ → List ℕ
  | Nat.zero => []
  | Nat.succ m =>
    let prev := nStepLucasList n m
    let next :=
      if m + 1 ≤ n then 2 ^ (m + 1) - 1
      else (prev.drop (prev.length - n)).foldl (· + ·) 0
    prev ++ [next]
Sources
Used by 1
Used byn-step Lucas numbers

Definitionn-step Lucas numbers#✓fully proved

For natural numbers \(n \ge 1\) and \(m\), the \(n\)-step Lucas number \(L^{(n)}_m\) is defined by \(L^{(n)}_0 = 0\), \(L^{(n)}_m = 2^m - 1\) for \(1 \le m \le n\), and \(L^{(n)}_m = \sum_{i=1}^{n} L^{(n)}_{m-i}\) for \(m \ge n + 1\). For \(n = 0\) we set \(L^{(0)}_m = 0\) for every \(m\).

The source defines \(L^{(n)}_m\) only for \(m \ge 1\); the value \(L^{(n)}_0 = 0\) is a convention.

def nStepLucas (n m : ℕ) : ℕ :=
  match n with
  | Nat.zero => 0
  | Nat.succ n => (nStepLucasList (n + 1) m).getLast?.getD 0
Sources
Uses 1
Statement usesFinite prefixes of the n-step Lucas numbers
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.