Filipponi's binomial sum

TheoremFilipponi's binomial-sum formula, without range conditions#✓fully proved

For natural numbers \(r\) and \(s\) let \(f_r(s) = \sum_{j=0}^{s} \binom{r-j}{j}\), where \(\binom{r-j}{j}\) is read as \(0\) when \(j > r\). Then for all natural numbers \(n\), \(h\) and \(k\), \(f_{n+2h}(k+h) = \sum_{j=0}^{h} \binom{h}{j} f_{n+j}(k+j)\).

The source states the formula under the condition \(0 \le k \le (n-h)/2\); with the convention above it holds for all \(n\), \(h\) and \(k\).

theorem filipponi_binomial_sum_formula_general
    (n h k : ℕ) :
    let f : ℕ → ℕ → ℕ := fun r s =>
      ∑ j ∈ Finset.range (s + 1), Nat.choose (r - j) j
    f (n + 2 * h) (k + h) =
      ∑ j ∈ Finset.range (h + 1), Nat.choose h j * f (n + j) (k + j)

Sources

• Hacène Belbachir and Amine Belkhir, "Combinatorial Expressions Involving Fibonacci, Hyperfibonacci, and Incomplete Fibonacci Numbers", Journal of Integer Sequences 17 (2014), Article 14.4.3, definition of f_r(s) at lines 304–319 and the formula at lines 347–371 of https://cs.uwaterloo.ca/journals/JIS/VOL17/Belbachir/belb2.tex; the formula is attributed there to P. Filipponi, "Incomplete Fibonacci and Lucas numbers", Rend. Circ. Mat. Palermo 45 (1996), 37–56, DOI 10.1007/BF02845088.

Used by 1

Used byFilipponi's binomial-sum formula

TheoremFilipponi's binomial-sum formula#✓fully proved

For natural numbers \(r\) and \(s\) let \(f_r(s) = \sum_{j=0}^{s} \binom{r-j}{j}\), where \(\binom{r-j}{j}\) is read as \(0\) when \(j > r\). If \(n\), \(h\) and \(k\) are natural numbers with \(h \le n\) and \(2k \le n - h\), then \(f_{n+2h}(k+h) = \sum_{j=0}^{h} \binom{h}{j} f_{n+j}(k+j)\).

The hypotheses encode the source condition \(0 \le k \le (n-h)/2\); the identity also holds without them.

theorem filipponi_binomial_sum_formula
    (n h k : ℕ) (hhn : h ≤ n) (hk : 2 * k ≤ n - h) :
    let f : ℕ → ℕ → ℕ := fun r s =>
      ∑ j ∈ Finset.range (s + 1), Nat.choose (r - j) j
    f (n + 2 * h) (k + h) =
      ∑ j ∈ Finset.range (h + 1), Nat.choose h j * f (n + j) (k + j)

Sources

• Hacène Belbachir and Amine Belkhir, "Combinatorial Expressions Involving Fibonacci, Hyperfibonacci, and Incomplete Fibonacci Numbers", Journal of Integer Sequences 17 (2014), Article 14.4.3, lines 347–371 of https://cs.uwaterloo.ca/journals/JIS/VOL17/Belbachir/belb2.tex; the formula is attributed there to P. Filipponi (1996).

Uses 1

Proof usesFilipponi's binomial-sum formula, without range conditions

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.