Generalized Delannoy numbers
TheoremDelannoy numbers as a sum of powers of two#●ready to prove
For all natural numbers \(m\) and \(n\), the Delannoy number \(D(m, n)\), that is, the Delannoy triangle entry \(T(m + n, m; 1)\), satisfies \(D(m, n) = \sum_{j=0}^{\min(m, n)} \binom{m}{j} \binom{n}{j} 2^j\).
public theorem_wanted delannoy_eq_sum_choose_mul_choose_two_pow (m n : ℕ) :
ordinaryRiordanPascalLikeMatrix (m + n) m 1 =
∑ j ∈ range (min m n + 1), (m.choose j : ℤ) * (n.choose j : ℤ) * 2 ^ j
public def ordinaryRiordanPascalLikeMatrix (n k : ℕ) (r : ℤ) : ℤ :=
Finset.sum (Finset.range (k + 1)) fun j =>
(k.choose j : ℤ) * ((n - j).choose k : ℤ) * r ^ j
MathlibExt/LinearAlgebra/Matrix/OrdinaryRiordanPascalLikeMatrix.lean:35
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 8 (
jis-2024-24.1.8-thm-8).
Uses 1
TheoremParity of a sum of adjacent binomial coefficients#●ready to prove
For all natural numbers \(n\) and \(k\) with \(k \ge 1\), \(\binom{n}{k} + \binom{n+1}{k} \equiv \binom{n}{k-1} \pmod 2\).
public theorem_wanted choose_add_choose_succ_modEq_two (n k : ℕ) (hk : 1 ≤ k) :
n.choose k + (n + 1).choose k ≡ n.choose (k - 1) [MOD 2]
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Lemma 15 (
jis-2024-24.1.8-lem-15).
DefinitionGeneralized Delannoy number with upper index#✓fully proved
For natural numbers \(k\), \(m\) and \(n\), the generalized Delannoy number \(D^k(m, n)\) is the natural number
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Section 1 (definition of
D^k(m, n)).
Used by 9
DefinitionLower generalized Delannoy number#✓fully proved
For natural numbers \(k\), \(m\) and \(n\), the generalized Delannoy number \(D_k(m, n)\) is
where each subtraction is truncated at \(0\). The definition is intended for \(m, n \ge k\), where no truncation occurs.
public def genDelannoyLower (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n - k - j).choose (n - k) * n.choose j
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Section 1 (definition of
D_k(m, n)).
Used by 5
TheoremAn upper generalized Delannoy number equal to \(13\)#✓fully proved
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. Then \(D^0(2, 2) = 13\).
public theorem genDelannoyUpper_zero_two_two : genDelannoyUpper 0 2 2 = 13
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Table 1.
Uses 1
TheoremAn upper generalized Delannoy number equal to \(44\)#✓fully proved
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. Then \(D^1(3, 2) = 44\).
public theorem genDelannoyUpper_one_three_two : genDelannoyUpper 1 3 2 = 44
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Table 1.
Uses 1
TheoremA value of the lower generalized Delannoy number#✓fully proved
The lower generalized Delannoy number \(D_1(2, 2)\) equals \(8\).
public theorem genDelannoyLower_one_two_two : genDelannoyLower 1 2 2 = 8
public def genDelannoyLower (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n - k - j).choose (n - k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:73
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Section 1 (central theorem
D_k(m, n) = 2^k D^k(n - k, m - k)).
Uses 1
TheoremThe lower and upper generalized Delannoy numbers agree at index zero#✓fully proved
For natural numbers \(k\), \(m\) and \(n\), let \(D_k(m, n) = \sum_{j=0}^{n} \binom{m + n - k - j}{n - k} \binom{n}{j}\) (with subtraction truncated at \(0\)) and \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) be the lower and upper generalized Delannoy numbers. Then \(D_0(m, n) = D^0(m, n)\) for all natural numbers \(m\) and \(n\).
public theorem genDelannoyLower_zero (m n : ℕ) : genDelannoyLower 0 m n = genDelannoyUpper 0 m n
public def genDelannoyLower (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n - k - j).choose (n - k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:73
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Section 1.
Uses 2
TheoremHorizontal sum identity for the upper generalized Delannoy numbers#●ready to prove
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. For all natural numbers \(k\), \(m\) and \(n\), \(D^k(m, n) + D^k(m, n + 1) = 2 D^{k+1}(m, n)\).
public theorem_wanted genDelannoyUpper_add_succ_right (k m n : ℕ) :
genDelannoyUpper k m n + genDelannoyUpper k m (n + 1) = 2 * genDelannoyUpper (k + 1) m n
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 3 (
jis-2024-24.1.8-thm-3).
Uses 1
TheoremVertical sum identity for the upper generalized Delannoy numbers#●ready to prove
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. For all natural numbers \(k\), \(m\) and \(n\) with \(k \ge 1\), \(D^k(m, n) + D^k(m + 1, n) = D^{k-1}(m + 1, n + 1)\).
public theorem_wanted genDelannoyUpper_add_succ_left (k m n : ℕ) (hk : 1 ≤ k) :
genDelannoyUpper k m n + genDelannoyUpper k (m + 1) n = genDelannoyUpper (k - 1) (m + 1) (n + 1)
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 4 (
jis-2024-24.1.8-thm-4).
Uses 1
TheoremHorizontal difference identity for the upper generalized Delannoy numbers#●ready to prove
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. For all natural numbers \(k\), \(m\) and \(n\) with \(m \ge 1\), \(D^k(m, n + 1) - D^k(m, n) = 2 D^{k+1}(m - 1, n)\).
public theorem_wanted genDelannoyUpper_succ_right_sub (k m n : ℕ) (hm : 1 ≤ m) :
(genDelannoyUpper k m (n + 1) : ℤ) - genDelannoyUpper k m n =
2 * genDelannoyUpper (k + 1) (m - 1) n
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Corollary 5 (
jis-2024-24.1.8-cor-5).
Uses 1
TheoremVertical difference identity for the upper generalized Delannoy numbers#●ready to prove
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. For all natural numbers \(k\), \(m\) and \(n\) with \(k \ge 1\), \(D^k(m + 1, n) - D^k(m, n) = D^{k-1}(m + 1, n)\).
public theorem_wanted genDelannoyUpper_succ_left_sub (k m n : ℕ) (hk : 1 ≤ k) :
(genDelannoyUpper k (m + 1) n : ℤ) - genDelannoyUpper k m n = genDelannoyUpper (k - 1) (m + 1) n
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Corollary 6 (
jis-2024-24.1.8-cor-6).
Uses 1
TheoremRelationship identities for generalized Delannoy numbers#●ready to prove
The four relationship identities for D_k (k ≥ 1, m, n ≥ k):
D_k(m, n) + D_k(m, n + 1) = 2 D_(k-1)(m, n), D_k(m, n) + D_k(m + 1, n) = D_(k+1)(m + 1, n + 1),
D_k(m, n + 1) - D_k(m, n) = 2 D_(k-1)(m - 1, n), D_k(m + 1, n) - D_k(m, n) = D_(k+1)(m + 1, n).
public theorem_wanted genDelannoyLower_relations (k m n : ℕ) (hk : 1 ≤ k) (hm : k ≤ m) (hn : k ≤ n) :
genDelannoyLower k m n + genDelannoyLower k m (n + 1) = 2 * genDelannoyLower (k - 1) m n ∧
genDelannoyLower k m n + genDelannoyLower k (m + 1) n =
genDelannoyLower (k + 1) (m + 1) (n + 1) ∧
(genDelannoyLower k m (n + 1) : ℤ) - genDelannoyLower k m n =
2 * genDelannoyLower (k - 1) (m - 1) n ∧
(genDelannoyLower k (m + 1) n : ℤ) - genDelannoyLower k m n = genDelannoyLower (k + 1) (m + 1) n
public def genDelannoyLower (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n - k - j).choose (n - k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:73
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 7 (
jis-2024-24.1.8-thm-7).
Uses 1
TheoremLower generalized Delannoy numbers as a sum of powers of two#●ready to prove
For natural numbers \(k\), \(m\), \(n\) with \(m \ge k\) and \(n \ge k\), the lower generalized Delannoy number \(D_k(m, n)\) satisfies \(D_k(m, n) = \sum_{j=0}^{\min(m-k, n-k)} \binom{m-k}{j} \binom{n}{j+k} 2^{j+k}\).
public theorem_wanted genDelannoyLower_eq_sum_two_pow (k m n : ℕ) (hm : k ≤ m) (hn : k ≤ n) :
genDelannoyLower k m n =
∑ j ∈ range (min (m - k) (n - k) + 1), (m - k).choose j * n.choose (j + k) * 2 ^ (j + k)
public def genDelannoyLower (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n - k - j).choose (n - k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:73
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 9 (
jis-2024-24.1.8-thm-9).
Uses 1
TheoremPowers-of-two formula for the upper generalized Delannoy numbers#●ready to prove
For natural numbers \(k\), \(m\) and \(n\), write \(D^k(m, n) = \sum_{j=0}^{n} \binom{m + n + k - j}{n + k} \binom{n}{j}\) for the upper generalized Delannoy numbers. For all natural numbers \(k\), \(m\) and \(n\),
public theorem_wanted genDelannoyUpper_eq_sum_two_pow (k m n : ℕ) :
genDelannoyUpper k m n = ∑ j ∈ range (min m n + 1), (m + k).choose (j + k) * n.choose j * 2 ^ j
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 10 (
jis-2024-24.1.8-thm-10).
Uses 1
TheoremUnified power-of-two sums for generalized Delannoy numbers#●ready to prove
For natural numbers \(k\), \(m\), \(n\), write \(D_k(m, n)\) and \(D^k(m, n)\) for the lower and upper generalized Delannoy numbers. If \(m \ge k\) and \(n \ge k\), then \(D_k(m, n) = \sum_{j=k}^{\min(m, n)} \binom{m-k}{j-k} \binom{n}{j} 2^j\); and, for all \(k\), \(m\), \(n\), \(D^k(m, n) = \sum_{j=0}^{\min(m, n)} \binom{m+k}{j+k} \binom{n}{j} 2^j\).
With the convention \(D_{-k} = D^k\), the second formula is the first with \(k\) replaced by \(-k\).
public theorem_wanted genDelannoy_eq_sum_two_pow_unified (k m n : ℕ) :
(k ≤ m → k ≤ n → genDelannoyLower k m n =
∑ j ∈ Ico k (min m n + 1), (m - k).choose (j - k) * n.choose j * 2 ^ j) ∧
genDelannoyUpper k m n = ∑ j ∈ range (min m n + 1), (m + k).choose (j + k) * n.choose j * 2 ^ j
public def genDelannoyLower (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n - k - j).choose (n - k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:73
public def genDelannoyUpper (k m n : ℕ) : ℕ :=
∑ j ∈ range (n + 1), (m + n + k - j).choose (n + k) * n.choose j
WantedExt/Combinatorics/Enumerative/DelannoyConstructionsWanted.lean:65
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 11 (
jis-2024-24.1.8-thm-11).
Uses 2
TheoremParity of adjacent rows of a Delannoy array#●ready to prove
Let \(R(m, n)\), for \(m, n \in \mathbb{N}\), be integers with \(R(m+1, n+1) = R(m, n+1) + R(m+1, n) + R(m, n)\) for all \(m, n\), and let \(m \in \mathbb{N}\). If \(R(m, 0) \equiv R(m+1, 0) \pmod 2\), then \(R(m, i) \equiv R(m+1, i) \pmod 2\) for all \(i\); if \(R(m, 0) \not\equiv R(m+1, 0) \pmod 2\), then \(R(m, i) \not\equiv R(m+1, i) \pmod 2\) for all \(i\).
public theorem_wanted delannoyArray_rows_parity (R : ℕ → ℕ → ℤ)
(hR : ∀ m n, R (m + 1) (n + 1) = R m (n + 1) + R (m + 1) n + R m n) (m : ℕ) :
(R m 0 ≡ R (m + 1) 0 [ZMOD 2] → ∀ i, R m i ≡ R (m + 1) i [ZMOD 2]) ∧
(¬ R m 0 ≡ R (m + 1) 0 [ZMOD 2] → ∀ i, ¬ R m i ≡ R (m + 1) i [ZMOD 2])
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 13 (
jis-2024-24.1.8-thm-13).
TheoremRows of iterated horizontal sums of a Delannoy array agree mod 2#●ready to prove
Let \(R(m, n)\), for \(m, n \in \mathbb{N}\), be integers with \(R(m+1, n+1) = R(m, n+1) + R(m+1, n) + R(m, n)\) for all \(m, n\). For an array \(S\) let \((HS)(m, n) = S(m, n) + S(m, n+1)\), and write \(R^i = H^i R\) for the \(i\)-fold horizontal sum. Then for every \(i \ge 1\) and all \(m, m', n \in \mathbb{N}\), \(R^i(m, n) \equiv R^i(m', n) \pmod 2\).
public theorem_wanted delannoyArray_horizontalSum_rows_modEq (R : ℕ → ℕ → ℤ)
(hR : ∀ m n, R (m + 1) (n + 1) = R m (n + 1) + R (m + 1) n + R m n) (i : ℕ) (hi : 1 ≤ i)
(m m' n : ℕ) :
(fun S : ℕ → ℕ → ℤ => fun a b => S a b + S a (b + 1))^[i] R m n ≡
(fun S : ℕ → ℕ → ℤ => fun a b => S a b + S a (b + 1))^[i] R m' n [ZMOD 2]
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Corollary 14 (
jis-2024-24.1.8-cor-14).
TheoremParity of iterated horizontal sums of a Delannoy array with binomial seeds#●ready to prove
Let \(R(m, n)\), for \(m, n \in \mathbb{N}\), be integers with \(R(m+1, n+1) = R(m, n+1) + R(m+1, n) + R(m, n)\) for all \(m, n\). For an array \(S\) let \((HS)(m, n) = S(m, n) + S(m, n+1)\), and write \(R^i = H^i R\) for the \(i\)-fold horizontal sum, so \(R^0 = R\). Let \(k \in \mathbb{N}\) and suppose \(R(0, n) = \binom{k+n}{k}\) for all \(n\); the values \(R(m, 0)\) for \(m \ge 1\) are arbitrary. Then every entry of \(R^{k+1}\) is even, and for every \(j \le k\) some entry of \(R^j\) is odd.
public theorem_wanted delannoyArray_binomial_seeds_parity (R : ℕ → ℕ → ℤ)
(hR : ∀ m n, R (m + 1) (n + 1) = R m (n + 1) + R (m + 1) n + R m n) (k : ℕ)
(hseed : ∀ n, R 0 n = (k + n).choose k) :
(∀ m n, (2 : ℤ) ∣ (fun S : ℕ → ℕ → ℤ => fun a b => S a b + S a (b + 1))^[k + 1] R m n) ∧
∀ j ≤ k, ∃ m n, ¬ (2 : ℤ) ∣ (fun S : ℕ → ℕ → ℤ => fun a b => S a b + S a (b + 1))^[j] R m n
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Lemma 16 (
jis-2024-24.1.8-lem-16).
TheoremFirst horizontal sums of a Delannoy array with binomial seeds#●ready to prove
Let \(R(m, n)\), for \(m, n \in \mathbb{N}\), be integers with \(R(m+1, n+1) = R(m, n+1) + R(m+1, n) + R(m, n)\) for all \(m, n\). Let \(k \ge 1\) and suppose \(R(0, n) = \binom{k+n}{k}\) for all \(n\). Then for all \(m\) and \(n\), \(R(m, n) + R(m, n+1) \equiv \binom{k+n}{k-1} \pmod 2\).
public theorem_wanted delannoyArray_binomial_seeds_horizontalSum_modEq (R : ℕ → ℕ → ℤ)
(hR : ∀ m n, R (m + 1) (n + 1) = R m (n + 1) + R (m + 1) n + R m n) (k : ℕ) (hk : 1 ≤ k)
(hseed : ∀ n, R 0 n = (k + n).choose k) (m n : ℕ) :
R m n + R m (n + 1) ≡ (k + n).choose (k - 1) [ZMOD 2]
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 17 (
jis-2024-24.1.8-thm-17).
TheoremPowers of two dividing iterated horizontal sums of a Delannoy array#●ready to prove
Let \(R(m, n)\), for \(m, n \in \mathbb{N}\), be integers with \(R(m+1, n+1) = R(m, n+1) + R(m+1, n) + R(m, n)\) for all \(m, n\). For an array \(S\) let \((HS)(m, n) = S(m, n) + S(m, n+1)\), and write \(R^i = H^i R\) for the \(i\)-fold horizontal sum. Let \(k, i \in \mathbb{N}\) with \(i \ge 1\), and suppose \(R(0, n) = \binom{k+n}{k}\) for all \(n\). Then every entry of \(R^{k+i}\) is divisible by \(2^i\), and some entry of \(R^{k+i}\) is not divisible by \(2^{i+1}\).
public theorem_wanted delannoyArray_binomial_seeds_two_pow_dvd (R : ℕ → ℕ → ℤ)
(hR : ∀ m n, R (m + 1) (n + 1) = R m (n + 1) + R (m + 1) n + R m n) (k i : ℕ) (hi : 1 ≤ i)
(hseed : ∀ n, R 0 n = (k + n).choose k) :
(∀ m n, (2 : ℤ) ^ i ∣ (fun S : ℕ → ℕ → ℤ => fun a b => S a b + S a (b + 1))^[k + i] R m n) ∧
∃ m n, ¬ (2 : ℤ) ^ (i + 1) ∣ (fun S : ℕ → ℕ → ℤ => fun a b => S a b + S a (b + 1))^[k + i] R m n
Sources
- Steven Edwards and William Griffiths, Delannoy Constructions, Journal of Integer Sequences 27 (2024), Article 24.1.8, Theorem 18 (
jis-2024-24.1.8-thm-18).
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.