Fibonacci p-numbers

DefinitionFibonacci p-numbers#✓fully proved

For a natural number \(p\), the Fibonacci \(p\)-numbers are the natural numbers \(F_p(r)\), \(r \in \mathbb{N}\), given by \(F_p(0) = 0\), \(F_p(r) = 1\) for \(1 \le r \le p\), and \(F_p(r) = F_p(r-1) + F_p(r-p-1)\) for \(r > p\).

def fibonacciP (p : ℕ) : ℕ → ℕ
  | 0 => 0
  | r + 1 =>
    if r + 1 ≤ p then 1 else fibonacciP p r + fibonacciP p (r - p)
termination_by r => r
decreasing_by
  · exact Nat.lt_succ_self _
  · exact Nat.lt_succ_of_le (Nat.sub_le _ _)
Sources
Used by 13
Used byCounting strongly restricted permutations with displacements \(-m\), \(0\), \(jm\) · Initial Fibonacci p-numbers equal one · Fibonacci 1-numbers are the Fibonacci numbers · Recurrence for Fibonacci p-numbers · Zeroth Fibonacci p-number · Honsberger identity for Fibonacci p-numbers · Fibonacci \(p\)-numbers as differences of \(A_p\) · Binomial sum formula for Fibonacci p-numbers · Generalized Leonardo \(p\)-numbers in terms of Fibonacci \(p\)-numbers · The sequence \(A_p\) as a sum of Fibonacci \(p\)-numbers · Sums of \(p+1\) consecutive Fibonacci \(p\)-numbers · Supergeneralized Leonardo p-numbers via Fibonacci p-numbers · Homogeneous supergeneralized Leonardo p-numbers via Fibonacci p-numbers

TheoremZeroth Fibonacci p-number#✓fully proved

For every natural number \(p\), the Fibonacci \(p\)-number \(F_p(0)\) equals \(0\).

@[simp]
theorem fibonacciP_zero (p : ℕ) : fibonacciP p 0 = 0
Uses 1 · Used by 1
Statement usesFibonacci p-numbers
Used byFibonacci 1-numbers are the Fibonacci numbers

TheoremInitial Fibonacci p-numbers equal one#✓fully proved

For all natural numbers \(p\) and \(r\) with \(1 \le r \le p\), the Fibonacci \(p\)-number \(F_p(r)\) equals \(1\).

theorem fibonacciP_eq_one (p r : ℕ) (hr : 1 ≤ r) (hrp : r ≤ p) : fibonacciP p r = 1
Uses 1
Statement usesFibonacci p-numbers

TheoremRecurrence for Fibonacci p-numbers#✓fully proved

For all natural numbers \(p\) and \(r\) with \(p < r\), the Fibonacci \(p\)-numbers satisfy \(F_p(r) = F_p(r-1) + F_p(r-p-1)\).

theorem fibonacciP_rec (p r : ℕ) (hpr : p < r) :
    fibonacciP p r = fibonacciP p (r - 1) + fibonacciP p (r - p - 1)
Uses 1 · Used by 1
Statement usesFibonacci p-numbers
Used byFibonacci 1-numbers are the Fibonacci numbers

TheoremFibonacci 1-numbers are the Fibonacci numbers#✓fully proved

For every natural number \(n\), the Fibonacci \(1\)-number \(F_1(n)\) equals the \(n\)-th Fibonacci number \(f_n\), where \(f_0 = 0\), \(f_1 = 1\) and \(f_{k+2} = f_{k+1} + f_k\).

theorem fibonacciP_one (n : ℕ) : fibonacciP 1 n = Nat.fib n
Uses 3
Statement usesFibonacci p-numbers
Proof usesRecurrence for Fibonacci p-numbers · Zeroth Fibonacci p-number

TheoremHonsberger identity for Fibonacci p-numbers#✓fully proved

Let \(p\), \(m\) and \(n\) be positive integers with \(p \le m + 1\) and \(p \le n + 2\), and write \(F_p(r)\) for the Fibonacci \(p\)-numbers. Suppose that \(F_p(0) = 0\), that \(F_p(r) = 1\) for \(1 \le r \le p\), and that \(F_p(r) = F_p(r-1) + F_p(r-p-1)\) for \(r > p\) (these hold by definition). Then

\[F_p(m+1)\,F_p(n+2) + \sum_{i=1}^{p} F_p(m+1-i)\,F_p(n+i+1-p) = F_p(m+n+2).\]

All indices in the sum are natural numbers, since \(i \le p \le m + 1\) and \(n + i + 1 \ge n + 2 \ge p\).

Proof: by strong induction on \(m\) from a uniform form of the recurrence, with a telescoping base case.

theorem honsberger_fibonacciP
    (p m n : ℕ) (hp : 0 < p) (hm_pos : 0 < m) (hn_pos : 0 < n)
    (hm : p ≤ m + 1) (hn : p ≤ n + 2) :
    fibonacciP p 0 = 0 →
    (∀ r, 1 ≤ r → r ≤ p → fibonacciP p r = 1) →
    (∀ r, p < r →
      fibonacciP p r =
        fibonacciP p (r - 1) + fibonacciP p (r - p - 1)) →
    fibonacciP p (m + 1) * fibonacciP p (n + 2) +
        ∑ j ∈ Finset.range p,
          fibonacciP p (m + 1 - (j + 1)) *
            fibonacciP p (n + (j + 1) + 1 - p) =
      fibonacciP p (m + n + 2)
Sources
Uses 1
Statement usesFibonacci p-numbers
6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.