Hypersequences

DefinitionHypersequence#✓fully proved

Let \((a_n)_{n \ge 0}\) be a sequence in an additive commutative monoid. Its hypersequence of generation \(r\), written \(a^{(r)}_n\), is defined by recursion on \(r\): \(a^{(0)}_n = a_n\) and \(a^{(r+1)}_n = \sum_{k=0}^{n} a^{(r)}_k\) for all natural numbers \(r\) and \(n\). Thus each generation is the sequence of partial sums of the previous one.

public def hypersequence {R : Type*} [AddCommMonoid R] (a : ℕ → R) : ℕ → ℕ → R
  | 0, n => a n
  | r + 1, n => ∑ k ∈ range (n + 1), hypersequence a r k

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Section 1, Equation (1.1).

Used by 12

Used byHypersequences through elementary symmetric polynomials · Hyperfibonacci numbers are the hypersequences of the Fibonacci numbers · Hyperlucas numbers in terms of Lucas numbers · Recurrence for the hyperlucas numbers · Hypersequences as binomial sums · First hypersequence at index zero · Each hypersequence generation sums the previous one · Recurrence between consecutive hypersequence generations · Abel summation by parts · Power-weighted sums of a sequence via its hypersequences · Power-weighted sums of hypersequences · Recurrence for power-weighted sums of hypersequences

TheoremEach hypersequence generation sums the previous one#✓fully proved

Let \((a_n)\) be a sequence in an additive commutative monoid and let \(a^{(r)}_n\) denote its hypersequence of generation \(r\). For all natural numbers \(r\) and \(n\), \(a^{(r+1)}_n = \sum_{k=0}^{n} a^{(r)}_k\).

public theorem hypersequence_succ {R : Type*} [AddCommMonoid R] (a : ℕ → R) (r n : ℕ) :
    hypersequence a (r + 1) n = ∑ k ∈ range (n + 1), hypersequence a r k

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Section 1, Equation (1.1).

Uses 1

Statement usesHypersequence

TheoremFirst hypersequence at index zero#✓fully proved

Let \((a_n)\) be a sequence in an additive commutative monoid and let \(a^{(1)}_n\) denote its hypersequence of generation \(1\). Then \(a^{(1)}_0 = a_0\).

public theorem hypersequence_one_zero {R : Type*} [AddCommMonoid R] (a : ℕ → R) :
    hypersequence a 1 0 = a 0

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Section 1, Equation (1.1).

Uses 1

Statement usesHypersequence

TheoremHyperfibonacci numbers are the hypersequences of the Fibonacci numbers#✓fully proved

Let \(F_k\) denote the \(k\)th Fibonacci number. For all natural numbers \(r\) and \(n\), the hyperfibonacci number \(F^{(r)}_n\) equals the \(r\)th hypersequence of the Fibonacci sequence at \(n\), that is, \(F^{(r)}_n = a^{(r)}_n\) for \(a_k = F_k\), where \(a^{(0)}_n = a_n\) and \(a^{(r+1)}_n = \sum_{k=0}^{n} a^{(r)}_k\).

public theorem hyperFibonacci_eq_hypersequence (r n : ℕ) :
    hyperFibonacci r n = hypersequence Nat.fib r n

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Example 3 (hyperfibonacci numbers).

Uses 2

Statement usesHyper-Fibonacci numbers · Hypersequence

DefinitionAlternating binomial power sum#✓fully proved

For natural numbers \(\ell, m\) and complex numbers \(x, y\),

\[p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell,\]

with the convention \(0^0 = 1\).

public def alternatingBinomialPowerSum (ℓ m : ℕ) (x y : ℂ) : ℂ :=
  ∑ k ∈ range (m + 1), (-1) ^ k * (m.choose k : ℂ) * (k * x + y) ^ ℓ

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Section 3, Equation (3.9).

Used by 14

Used byBoyadzhiev's and Katsuura's formulas for alternating binomial power sums · A value of the alternating binomial power sum · Recurrences for alternating binomial power sums · Small cases of alternating binomial power sums · Special values of alternating binomial power sums · Derivative and recurrence of the shifted alternating binomial power sums · The inverse of Parisse's matrix \(B(n)\) · The inverse of Parisse's matrix \(C(n)\) · Parisse's coefficients at \(n\) from their values at \(-1\) · The product of Parisse's matrices B(n) and C(n) · Power-weighted sums of a sequence via its hypersequences · Power-weighted sums of Fibonacci numbers · Power-weighted sums of hypersequences · Power-weighted sums of Lucas numbers

TheoremA value of the alternating binomial power sum#✓fully proved

The alternating binomial power sum \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell\) satisfies \(p_{1,1}(1, 1) = 1 - 2 = -1\).

public theorem alternatingBinomialPowerSum_one_one_one_one :
    alternatingBinomialPowerSum 1 1 1 1 = -1

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Section 3, Equation (3.9).

Uses 1

Statement usesAlternating binomial power sum

TheoremHypersequences as binomial sums#●ready to prove

Let \((a_n)\) be a sequence of complex numbers and let \(a^{(r)}_n\) denote its hypersequence of generation \(r\). For every \(r \ge 1\) and every natural number \(n\),

\[a^{(r)}_n = \sum_{k=0}^{n} \binom{n+r-1-k}{r-1} a_k = \sum_{k=0}^{n} \binom{r+k-1}{k} a_{n-k}.\]

public theorem_wanted hypersequence_eq_sum_choose (a : ℕ → ℂ) {r : ℕ} (hr : 1 ≤ r) (n : ℕ) :
    hypersequence a r n = ∑ k ∈ range (n + 1), ((n + r - 1 - k).choose (r - 1) : ℂ) * a k ∧
      hypersequence a r n = ∑ k ∈ range (n + 1), ((r + k - 1).choose k : ℂ) * a (n - k)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 1, Equation (2.1).

Uses 1

Statement usesHypersequence

TheoremRecurrence between consecutive hypersequence generations#●ready to prove

Let \((a_n)\) be a sequence of complex numbers and let \(a^{(r)}_n\) denote its hypersequence of generation \(r\). For all natural numbers \(r\) and \(n\), \(a^{(r+1)}_{n+1} = a^{(r+1)}_n + a^{(r)}_{n+1}\).

public theorem_wanted hypersequence_succ_succ (a : ℕ → ℂ) (r n : ℕ) :
    hypersequence a (r + 1) (n + 1) = hypersequence a (r + 1) n + hypersequence a r (n + 1)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 2, Equation (2.2).

Uses 1

Statement usesHypersequence

TheoremHyperfibonacci numbers in terms of Fibonacci numbers#●ready to prove

Let \(F_k\) denote the \(k\)th Fibonacci number and \(F^{(r)}_n\) the hyperfibonacci numbers, given by \(F^{(0)}_n = F_n\) and \(F^{(r+1)}_n = \sum_{k=0}^{n} F^{(r)}_k\). For all natural numbers \(r\) and \(n\),

\[F^{(r)}_n = F_{n+2r} - \sum_{k=0}^{r-1} \binom{n + k - 1}{k} F_{2(r-k)}.\]

public theorem_wanted hyperFibonacci_eq_fib_sub_sum (r n : ℕ) :
    (hyperFibonacci r n : ℤ) =
      Nat.fib (n + 2 * r) - ∑ k ∈ range r, ((n + k - 1).choose k * Nat.fib (2 * (r - k)) : ℕ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 3, Equation (2.8).

Uses 1

Statement usesHyper-Fibonacci numbers

TheoremFibonacci numbers as binomially weighted sums#●ready to prove

Let \(F_k\) denote the \(k\)th Fibonacci number. For every natural number \(r \ge 1\) and every natural number \(n\),

\[F_{n+2r} = \sum_{k=0}^{n} \binom{n + r - 1 - k}{r - 1} F_k + \sum_{k=0}^{r-1} \binom{n + k - 1}{k} F_{2(r-k)}\]

and

\[F_{n+2r} = \sum_{k=0}^{n} \binom{r + k - 1}{k} F_{n-k} + \sum_{k=0}^{r-1} \binom{n + k - 1}{k} F_{2(r-k)}.\]

public theorem_wanted fib_add_two_mul_eq_sum_choose {r : ℕ} (hr : 1 ≤ r) (n : ℕ) :
    Nat.fib (n + 2 * r) = ∑ k ∈ range (n + 1), (n + r - 1 - k).choose (r - 1) * Nat.fib k +
        ∑ k ∈ range r, (n + k - 1).choose k * Nat.fib (2 * (r - k)) ∧
      Nat.fib (n + 2 * r) = ∑ k ∈ range (n + 1), (r + k - 1).choose k * Nat.fib (n - k) +
        ∑ k ∈ range r, (n + k - 1).choose k * Nat.fib (2 * (r - k))

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Corollary 1.

TheoremRecurrence for the hyperfibonacci numbers#●ready to prove

Let \(F^{(r)}_n\) denote the hyperfibonacci numbers. For all natural numbers \(r\) and \(n\), \(F^{(r)}_0 = 0\), \(F^{(r)}_1 = 1\), and \(F^{(r+1)}_{n+2} = F^{(r+1)}_{n+1} + F^{(r+1)}_n + \binom{n+r+1}{r}\).

Equivalently, for \(r \ge 1\), \(F^{(r)}_{n+2} = F^{(r)}_{n+1} + F^{(r)}_n + \binom{n+r}{r-1}\), the form in which Parisse quotes this result of Cristea, Martinjak and Urbiha.

public theorem_wanted hyperFibonacci_recurrence (r n : ℕ) :
    hyperFibonacci r 0 = 0 ∧ hyperFibonacci r 1 = 1 ∧
      hyperFibonacci (r + 1) (n + 2) =
        hyperFibonacci (r + 1) (n + 1) + hyperFibonacci (r + 1) n + (n + r + 1).choose r

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 4, Equation (2.9).

Uses 1

Statement usesHyper-Fibonacci numbers

TheoremHyperlucas numbers in terms of Lucas numbers#●ready to prove

Let \(L_n\) denote the Lucas numbers and let \(L^{(r)}_n\) denote the hyperlucas numbers, the hypersequence of generation \(r\) of \((L_n)\). For all natural numbers \(r\) and \(n\), in the integers,

\[L^{(r)}_n = L_{n+2r} - \sum_{k=0}^{r-1} \binom{n+k}{k} L_{2(r-k)-1}.\]

public theorem_wanted hyperLucas_eq_lucas_sub_sum (r n : ℕ) :
    ((hypersequence lucasNumber r n : ℕ) : ℤ) =
      lucasNumber (n + 2 * r) -
        ∑ k ∈ range r, ((n + k).choose k * lucasNumber (2 * (r - k) - 1) : ℕ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 5, Equation (2.12).

Uses 2

Statement usesHypersequence · Lucas numbers

TheoremLucas numbers as binomial sums#●ready to prove

Let \(L_n\) denote the Lucas numbers. For every \(r \ge 1\) and every natural number \(n\),

\[L_{n+2r} = \sum_{k=0}^{n} \binom{n+r-1-k}{r-1} L_k + \sum_{k=0}^{r-1} \binom{n+k}{k} L_{2(r-k)-1}\]

and

\[L_{n+2r} = \sum_{k=0}^{n} \binom{r+k-1}{k} L_{n-k} + \sum_{k=0}^{r-1} \binom{n+k}{k} L_{2(r-k)-1}.\]

public theorem_wanted lucas_add_two_mul_eq_sum_choose {r : ℕ} (hr : 1 ≤ r) (n : ℕ) :
    lucasNumber (n + 2 * r) =
        ∑ k ∈ range (n + 1), (n + r - 1 - k).choose (r - 1) * lucasNumber k +
          ∑ k ∈ range r, (n + k).choose k * lucasNumber (2 * (r - k) - 1) ∧
      lucasNumber (n + 2 * r) =
        ∑ k ∈ range (n + 1), (r + k - 1).choose k * lucasNumber (n - k) +
          ∑ k ∈ range r, (n + k).choose k * lucasNumber (2 * (r - k) - 1)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Corollary 2.

Uses 1

Statement usesLucas numbers

TheoremRecurrence for the hyperlucas numbers#●ready to prove

Let \(L^{(r)}_n\) denote the hyperlucas numbers, the hypersequence of generation \(r\) of the Lucas numbers. For all natural numbers \(r\) and \(n\), \(L^{(r)}_0 = 2\), \(L^{(r)}_1 = 2r + 1\), and, in the rational numbers,

\[L^{(r+1)}_{n+2} = L^{(r+1)}_{n+1} + L^{(r+1)}_n + \frac{n + 2(r+1)}{n+2} \binom{n+r+1}{r}.\]

Equivalently, for \(r \ge 1\),

\[L^{(r)}_{n+2} = L^{(r)}_{n+1} + L^{(r)}_n + \frac{n+2r}{n+2} \binom{n+r}{r-1}.\]

public theorem_wanted hyperLucas_recurrence (r n : ℕ) :
    hypersequence lucasNumber r 0 = 2 ∧ hypersequence lucasNumber r 1 = 2 * r + 1 ∧
      ((hypersequence lucasNumber (r + 1) (n + 2) : ℕ) : ℚ) =
        ((hypersequence lucasNumber (r + 1) (n + 1) : ℕ) : ℚ) +
          ((hypersequence lucasNumber (r + 1) n : ℕ) : ℚ) +
          ((n + 2 * (r + 1) : ℕ) : ℚ) / (n + 2) * ((n + r + 1).choose r : ℚ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 6, Equation (2.13).

Uses 2

Statement usesHypersequence · Lucas numbers

TheoremAbel summation by parts#●ready to prove

Let \(a\) and \(b\) be sequences of complex numbers and let \(a^{(1)}_k = \sum_{i=0}^{k} a_i\) be the first hypersequence (the partial sums) of \(a\). Then for every natural number \(n\),

\[\sum_{k=0}^{n} a_k b_k = a^{(1)}_n b_{n+1} + \sum_{k=0}^{n} a^{(1)}_k (b_k - b_{k+1}).\]

public theorem_wanted sum_mul_eq_hypersequence_one_mul_add_sum (a b : ℕ → ℂ) (n : ℕ) :
    ∑ k ∈ range (n + 1), a k * b k =
      hypersequence a 1 n * b (n + 1) + ∑ k ∈ range (n + 1), hypersequence a 1 k * (b k - b (k + 1))

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 7.

Uses 1

Statement usesHypersequence

TheoremRecurrence for power-weighted sums of hypersequences#●ready to prove

Let \(a\) be a sequence of complex numbers, let \(a^{(r)}_k\) denote its hypersequence of generation \(r\), and for natural numbers \(\ell\), \(r\) and \(n\) let \(t^{(r)}_\ell(n) = \sum_{k=0}^{n} k^\ell a^{(r)}_k\), with the convention \(0^0 = 1\). Then for all natural numbers \(\ell\), \(r\) and \(n\),

\[t^{(r)}_\ell(n) = (n + 1)^\ell a^{(r+1)}_n - \sum_{j=0}^{\ell-1} \binom{\ell}{j} t^{(r+1)}_j(n),\]

where the sum over \(j\) is empty when \(\ell = 0\).

public theorem_wanted sum_pow_mul_hypersequence_recurrence (a : ℕ → ℂ) (ℓ r n : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * hypersequence a r k =
      ((n : ℂ) + 1) ^ ℓ * hypersequence a (r + 1) n -
        ∑ j ∈ range ℓ, (ℓ.choose j : ℂ) *
          ∑ k ∈ range (n + 1), (k : ℂ) ^ j * hypersequence a (r + 1) k

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 8, Equation (3.5).

Uses 1

Statement usesHypersequence

TheoremPower-weighted sums of hypersequences#●ready to prove

Let \(a\) be a sequence of complex numbers, let \(a^{(r)}_n\) denote its hypersequence of generation \(r\), let \(p_{\ell,m}(x, y) = \sum_{i=0}^{m} (-1)^i \binom{m}{i} (ix + y)^\ell\) be the alternating binomial power sum, and let \(S(j, m)\) denote the Stirling numbers of the second kind. Then for all natural numbers \(\ell\), \(n\) and \(r\), with the convention \(0^0 = 1\),

\[\sum_{k=0}^{n} k^\ell a^{(r)}_k = \sum_{m=0}^{\ell} p_{\ell,m}(1, n + 1)\, a^{(r+m+1)}_n\]

and

\[\sum_{k=0}^{n} k^\ell a^{(r)}_k = \sum_{j=0}^{\ell} \binom{\ell}{j} \Bigl(\sum_{m=0}^{j} (-1)^m\, m!\, S(j, m)\, a^{(r+m+1)}_n\Bigr) (n + 1)^{\ell-j}.\]

public theorem_wanted sum_pow_mul_hypersequence_eq (a : ℕ → ℂ) (ℓ n r : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * hypersequence a r k =
        ∑ m ∈ range (ℓ + 1),
          alternatingBinomialPowerSum ℓ m 1 (n + 1) * hypersequence a (r + m + 1) n ∧
      ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * hypersequence a r k =
        ∑ j ∈ range (ℓ + 1), (ℓ.choose j : ℂ) *
          (∑ m ∈ range (j + 1), (-1) ^ m * (m.factorial : ℂ) * (Nat.stirlingSecond j m : ℂ) *
            hypersequence a (r + m + 1) n) * ((n : ℂ) + 1) ^ (ℓ - j)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 9, Equations (3.7) and (3.8).

Uses 2

Statement usesAlternating binomial power sum · Hypersequence

TheoremPower-weighted sums of a sequence via its hypersequences#●ready to prove

Let \(a\) be a sequence of complex numbers, let \(a^{(r)}_n\) denote its hypersequence of generation \(r\), let \(p_{\ell,m}(x, y) = \sum_{i=0}^{m} (-1)^i \binom{m}{i} (ix + y)^\ell\) be the alternating binomial power sum, and let \(S(j, m)\) denote the Stirling numbers of the second kind. Then for all natural numbers \(\ell\) and \(n\), with the convention \(0^0 = 1\),

\[\sum_{k=0}^{n} k^\ell a_k = \sum_{m=0}^{\ell} p_{\ell,m}(1, n + 1)\, a^{(m+1)}_n\]

and

\[\sum_{k=0}^{n} k^\ell a_k = \sum_{j=0}^{\ell} \binom{\ell}{j} \Bigl(\sum_{m=0}^{j} (-1)^m\, m!\, S(j, m)\, a^{(m+1)}_n\Bigr) (n + 1)^{\ell-j}.\]

This is the case \(r = 0\) of the corresponding identity for \(\sum_{k=0}^{n} k^\ell a^{(r)}_k\).

public theorem_wanted sum_pow_mul_eq (a : ℕ → ℂ) (ℓ n : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * a k =
        ∑ m ∈ range (ℓ + 1), alternatingBinomialPowerSum ℓ m 1 (n + 1) * hypersequence a (m + 1) n ∧
      ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * a k =
        ∑ j ∈ range (ℓ + 1), (ℓ.choose j : ℂ) *
          (∑ m ∈ range (j + 1), (-1) ^ m * (m.factorial : ℂ) * (Nat.stirlingSecond j m : ℂ) *
            hypersequence a (m + 1) n) * ((n : ℂ) + 1) ^ (ℓ - j)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Corollary 3.

Uses 2

Statement usesAlternating binomial power sum · Hypersequence

TheoremBoyadzhiev's and Katsuura's formulas for alternating binomial power sums#●ready to prove

Let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell\) and let \(S(j, m)\) denote the Stirling numbers of the second kind. For all complex numbers \(x, y\) and natural numbers \(\ell, m\): (i) (Boyadzhiev) \(p_{\ell,m}(x, y) = \sum_{j=m}^{\ell} \binom{\ell}{j} (-1)^m m!\, S(j, m)\, x^j y^{\ell-j}\), where the sum is empty (hence \(0\)) when \(\ell < m\); (ii) (Katsuura) if \(\ell < m\) then \(p_{\ell,m}(x, y) = 0\), and \(p_{m,m}(x, y) = (-1)^m x^m m!\).

public theorem_wanted alternatingBinomialPowerSum_eq_sum_stirlingSecond (x y : ℂ) (ℓ m : ℕ) :
    alternatingBinomialPowerSum ℓ m x y =
        ∑ j ∈ Icc m ℓ, (ℓ.choose j : ℂ) * (-1) ^ m * (m.factorial : ℂ) *
          (Nat.stirlingSecond j m : ℂ) * x ^ j * y ^ (ℓ - j) ∧
      (ℓ < m → alternatingBinomialPowerSum ℓ m x y = 0) ∧
      alternatingBinomialPowerSum m m x y = (-1) ^ m * x ^ m * (m.factorial : ℂ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Proposition 1.

Uses 1

Statement usesAlternating binomial power sum

TheoremSpecial values of alternating binomial power sums#●ready to prove

Let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell\), with \(0^0 = 1\), and let \(S(j, m)\) denote the Stirling numbers of the second kind. For all complex numbers \(x, y\) and natural numbers \(\ell, m\): (i) \(p_{\ell,m}(x, x) = (-1)^m m!\, S(\ell + 1, m + 1)\, x^\ell\), and in particular \(p_{\ell,m}(1, 1) = (-1)^m m!\, S(\ell + 1, m + 1)\); (ii) \(p_{\ell,m}(0, y) = 0^m y^\ell\); (iii) \(p_{\ell,m}(x, 0) = (-1)^m m!\, S(\ell, m)\, x^\ell\), and in particular \(p_{m+1,m}(1, 0) = (-1)^m m! \binom{m+1}{2}\); (iv) \(p_{\ell,m}(-1, m) = m!\, S(\ell, m)\).

public theorem_wanted alternatingBinomialPowerSum_special_values (x y : ℂ) (ℓ m : ℕ) :
    alternatingBinomialPowerSum ℓ m x x =
        (-1) ^ m * (m.factorial : ℂ) * (Nat.stirlingSecond (ℓ + 1) (m + 1) : ℂ) * x ^ ℓ ∧
      alternatingBinomialPowerSum ℓ m 1 1 =
        (-1) ^ m * (m.factorial : ℂ) * (Nat.stirlingSecond (ℓ + 1) (m + 1) : ℂ) ∧
      alternatingBinomialPowerSum ℓ m 0 y = 0 ^ m * y ^ ℓ ∧
      alternatingBinomialPowerSum ℓ m x 0 =
        (-1) ^ m * (m.factorial : ℂ) * (Nat.stirlingSecond ℓ m : ℂ) * x ^ ℓ ∧
      alternatingBinomialPowerSum (m + 1) m 1 0 =
        (-1) ^ m * (m.factorial : ℂ) * ((m + 1).choose 2 : ℂ) ∧
      alternatingBinomialPowerSum ℓ m (-1) m = (m.factorial : ℂ) * (Nat.stirlingSecond ℓ m : ℂ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Proposition 2 (i)–(iv).

Uses 1

Statement usesAlternating binomial power sum

TheoremSmall cases of alternating binomial power sums#●ready to prove

Let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell\), with \(0^0 = 1\). For all complex numbers \(x, y\) and natural numbers \(\ell, m\): (i) \(p_{\ell,0}(x, y) = y^\ell\); (ii) \(p_{\ell,1}(x, y) = y^\ell - (x + y)^\ell\); (iii) \(p_{\ell,2}(x, y) = y^\ell - 2(x + y)^\ell + (2x + y)^\ell\); (iv) if \(\ell \ge 1\), then \(p_{\ell,\ell-1}(x, y) = (-1)^{\ell-1} \ell!\, x^{\ell-1} \left(y + \frac{\ell - 1}{2} x\right)\); (v) \(p_{\ell,\ell}(x, y) = (-1)^\ell \ell!\, x^\ell\); (vi) \(p_{0,m}(x, y) = 0^m\); (vii) \(\sum_{m=0}^{\ell} p_{\ell,m}(x, y) = (y - x)^\ell\).

public theorem_wanted alternatingBinomialPowerSum_small_cases (x y : ℂ) (ℓ m : ℕ) :
    alternatingBinomialPowerSum ℓ 0 x y = y ^ ℓ ∧
      alternatingBinomialPowerSum ℓ 1 x y = y ^ ℓ - (x + y) ^ ℓ ∧
      alternatingBinomialPowerSum ℓ 2 x y = y ^ ℓ - 2 * (x + y) ^ ℓ + (2 * x + y) ^ ℓ ∧
      (1 ≤ ℓ → alternatingBinomialPowerSum ℓ (ℓ - 1) x y =
        (-1) ^ (ℓ - 1) * (ℓ.factorial : ℂ) * x ^ (ℓ - 1) * (y + ((ℓ : ℂ) - 1) / 2 * x)) ∧
      alternatingBinomialPowerSum ℓ ℓ x y = (-1) ^ ℓ * (ℓ.factorial : ℂ) * x ^ ℓ ∧
      alternatingBinomialPowerSum 0 m x y = 0 ^ m ∧
      ∑ m ∈ range (ℓ + 1), alternatingBinomialPowerSum ℓ m x y = (y - x) ^ ℓ

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Proposition 3.

Uses 1

Statement usesAlternating binomial power sum

TheoremRecurrences for alternating binomial power sums#●ready to prove

Let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell\). For all complex numbers \(x, y\) and natural numbers \(\ell, m\) (sums over an empty range are \(0\), and \(m - 1\) means \(0\) when \(m = 0\)): (i) \(p_{\ell,m+1}(x, y) = p_{\ell,m}(x, y) - p_{\ell,m}(x, x + y)\); (ii) \(p_{\ell,m}(x, x + y) = \sum_{j=m}^{\ell} \binom{\ell}{j} p_{j,m}(x, y)\, x^{\ell-j}\); (iii) \(p_{\ell,m+1}(x, y) = -\sum_{j=m}^{\ell-1} \binom{\ell}{j} p_{j,m}(x, y)\, x^{\ell-j}\); (iv) \(p_{\ell+1,m}(x, y) = y\, p_{\ell,m}(x, y) - m x\, p_{\ell,m-1}(x, x + y)\); (v) \(p_{\ell+1,m+1}(x, y) = ((m + 1) x + y)\, p_{\ell,m+1}(x, y) - (m + 1) x\, p_{\ell,m}(x, y)\); (vi) if \(\ell \ge 1\), the complex derivative of \(z \mapsto p_{\ell,m}(x, z)\) at \(z = y\) is \(\ell\, p_{\ell-1,m}(x, y)\); (vii) if \(\ell \ge 1\), then \(p_{\ell,m}(x, y) = (m x + y)\, p_{\ell-1,m}(x, y) - m x\, p_{\ell-1,m-1}(x, y)\).

MetaMathlibExt.alternatingBinomialPowerSum_recurrences · 18 lines

public theorem_wanted alternatingBinomialPowerSum_recurrences (x y : ℂ) (ℓ m : ℕ) :
    alternatingBinomialPowerSum ℓ (m + 1) x y =
        alternatingBinomialPowerSum ℓ m x y - alternatingBinomialPowerSum ℓ m x (x + y) ∧
      alternatingBinomialPowerSum ℓ m x (x + y) =
        ∑ j ∈ Icc m ℓ, (ℓ.choose j : ℂ) * alternatingBinomialPowerSum j m x y * x ^ (ℓ - j) ∧
      alternatingBinomialPowerSum ℓ (m + 1) x y =
        -∑ j ∈ Ico m ℓ, (ℓ.choose j : ℂ) * alternatingBinomialPowerSum j m x y * x ^ (ℓ - j) ∧
      alternatingBinomialPowerSum (ℓ + 1) m x y =
        y * alternatingBinomialPowerSum ℓ m x y -
          m * x * alternatingBinomialPowerSum ℓ (m - 1) x (x + y) ∧
      alternatingBinomialPowerSum (ℓ + 1) (m + 1) x y =
        ((m + 1) * x + y) * alternatingBinomialPowerSum ℓ (m + 1) x y -
          (m + 1) * x * alternatingBinomialPowerSum ℓ m x y ∧
      (1 ≤ ℓ → deriv (fun z => alternatingBinomialPowerSum ℓ m x z) y =
        ℓ * alternatingBinomialPowerSum (ℓ - 1) m x y) ∧
      (1 ≤ ℓ → alternatingBinomialPowerSum ℓ m x y =
        (m * x + y) * alternatingBinomialPowerSum (ℓ - 1) m x y -
          m * x * alternatingBinomialPowerSum (ℓ - 1) (m - 1) x y)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Proposition 4.

Uses 1

Statement usesAlternating binomial power sum

TheoremDerivative and recurrence of the shifted alternating binomial power sums#●ready to prove

Let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (kx + y)^\ell\) and, for a complex number \(n\), let \(c_{\ell,m}(n) = p_{\ell,m}(1, n + 1)\). For natural numbers \(\ell, m \ge 1\) and every complex number \(n\), the complex derivative of \(c_{\ell,m}\) at \(n\) is \(\ell\, c_{\ell-1,m}(n)\), and \(c_{\ell,m}(n) = (m + n + 1)\, c_{\ell-1,m}(n) - m\, c_{\ell-1,m-1}(n)\).

The variable \(n\) is complex here because the paper differentiates in \(n\).

public theorem_wanted carlitzSum_deriv_and_recurrence {ℓ m : ℕ} (hℓ : 1 ≤ ℓ) (hm : 1 ≤ m)
    (n : ℂ) :
    deriv (fun z => alternatingBinomialPowerSum ℓ m 1 (z + 1)) n =
        ℓ * alternatingBinomialPowerSum (ℓ - 1) m 1 (n + 1) ∧
      alternatingBinomialPowerSum ℓ m 1 (n + 1) =
        (m + n + 1) * alternatingBinomialPowerSum (ℓ - 1) m 1 (n + 1) -
          m * alternatingBinomialPowerSum (ℓ - 1) (m - 1) 1 (n + 1)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Corollary 4, Equation (3.38).

Uses 1

Statement usesAlternating binomial power sum

TheoremSums of \(m\)th powers via Stirling numbers of the second kind#●ready to prove

For all natural numbers \(n\) and \(m\),

\[\sum_{k=1}^{n} k^m = \sum_{k=0}^{m} (-1)^{m-k}\, k!\, \binom{n + k}{k + 1}\, S(m, k),\]

where \(S(m, k)\) denotes the Stirling numbers of the second kind.

The paper takes \(n \ge 1\); for \(n = 0\) both sides vanish, so that case is included.

public theorem_wanted sum_pow_eq_sum_stirlingSecond (n m : ℕ) :
    ∑ k ∈ Icc 1 n, (k : ℤ) ^ m =
      ∑ k ∈ range (m + 1),
        (-1) ^ (m - k) * (k.factorial : ℤ) * ((n + k).choose (k + 1) : ℤ) *
          (Nat.stirlingSecond m k : ℤ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Corollary 5, Equation (4.4).

TheoremAlternating binomial expansion of a shifted binomial coefficient#●ready to prove

For all natural numbers \(m\), \(n\) and \(k\),

\[\binom{n+m-k-1}{m} = \sum_{j=0}^{k} (-1)^j \binom{k}{j} \binom{n+m-j-1}{m-j},\]

where, for an integer \(x\) and a natural number \(i\), \(\binom{x}{i} = x(x-1)\cdots(x-i+1)/i!\) is the generalized binomial coefficient, and the term \(\binom{n+m-j-1}{m-j}\) is taken to be \(0\) when \(j > m\).

public theorem_wanted ringChoose_sub_eq_sum (m n k : ℕ) :
    Ring.choose ((n : ℤ) + m - k - 1) m =
      ∑ j ∈ range (k + 1), (-1) ^ j * (k.choose j : ℤ) *
        (if j ≤ m then Ring.choose ((n : ℤ) + m - j - 1) (m - j) else 0)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Lemma 1, Equation (4.10).

TheoremPowers of \(k + 1\) via Stirling numbers of the second kind#●ready to prove

For all natural numbers \(k\) and \(\ell\),

\[(k + 1)^\ell = \sum_{j=0}^{k} \binom{k}{j}\, j!\, S(\ell + 1, j + 1),\]

where \(S(i, j)\) denotes the Stirling numbers of the second kind.

public theorem_wanted succ_pow_eq_sum_stirlingSecond (k ℓ : ℕ) :
    (k + 1) ^ ℓ = ∑ j ∈ range (k + 1), k.choose j * j.factorial * Nat.stirlingSecond (ℓ + 1) (j + 1)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Lemma 2, Equation (4.11).

TheoremPower-weighted sums of Fibonacci numbers#●ready to prove

Let \(F_k\) denote the Fibonacci numbers and let \(p_{\ell,m}(x, y) = \sum_{i=0}^{m} (-1)^i \binom{m}{i} (ix + y)^\ell\) be the alternating binomial power sum. Then for all natural numbers \(\ell\) and \(n\), with the convention \(0^0 = 1\),

\[\sum_{k=0}^{n} k^\ell F_k = \sum_{m=0}^{\ell} p_{\ell,m}(1, n + 1)\, F_{n+2(m+1)} - \sum_{m=0}^{\ell} p_{\ell,m}(1, 1)\, F_{2(m+1)}.\]

The paper's conjecture on the constant term, stated after this theorem, is not included.

public theorem_wanted sum_pow_mul_fib_eq (ℓ n : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * Nat.fib k =
      ∑ m ∈ range (ℓ + 1), alternatingBinomialPowerSum ℓ m 1 (n + 1) * Nat.fib (n + 2 * (m + 1)) -
        ∑ m ∈ range (ℓ + 1), alternatingBinomialPowerSum ℓ m 1 1 * Nat.fib (2 * (m + 1))

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 10, Equation (4.7).

Uses 1

Statement usesAlternating binomial power sum

TheoremPower-weighted sums of Lucas numbers#●ready to prove

Let \(L_k\) denote the Lucas numbers, so \(L_0 = 2\), \(L_1 = 1\) and \(L_{k+2} = L_{k+1} + L_k\), and let \(p_{\ell,m}(x, y) = \sum_{i=0}^{m} (-1)^i \binom{m}{i} (ix + y)^\ell\) be the alternating binomial power sum. Then for all natural numbers \(\ell\) and \(n\), with the convention \(0^0 = 1\),

\[\sum_{k=0}^{n} k^\ell L_k = \sum_{m=0}^{\ell} p_{\ell,m}(1, n + 1)\, L_{n+2(m+1)} - \sum_{m=0}^{\ell} p_{\ell,m}(1, 1)\, L_{2(m+1)} + L_0 \cdot 0^\ell.\]

The paper's conjecture on the constant term, stated after this theorem, is not included.

public theorem_wanted sum_pow_mul_lucas_eq (ℓ n : ℕ) :
    ∑ k ∈ range (n + 1), (k : ℂ) ^ ℓ * lucasNumber k =
      ∑ m ∈ range (ℓ + 1),
          alternatingBinomialPowerSum ℓ m 1 (n + 1) * lucasNumber (n + 2 * (m + 1)) -
        ∑ m ∈ range (ℓ + 1), alternatingBinomialPowerSum ℓ m 1 1 * lucasNumber (2 * (m + 1)) +
        lucasNumber 0 * 0 ^ ℓ

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums, INTEGERS 24 (2024), Article A70, Theorem 11, Equation (4.9).

Uses 2

Statement usesAlternating binomial power sum · Lucas numbers

TheoremRecurrence, closed form and row sums of \(e_{j,k}(n)\)#●ready to prove

Let \(n \in \mathbb{N}\) and let \(e_{j,k}(n)\) be the elementary symmetric polynomial of degree \(k\) in \(n + 1, \dots, n + j\). Write \([j, \ell]\) for the unsigned Stirling numbers of the first kind and \(x^{\overline{j}} = x (x + 1) \cdots (x + j - 1)\) for the rising factorial. Then \(e_{0,k}(n) = \delta_{0,k}\) for all \(k\); \(e_{j+1,k+1}(n) = e_{j,k+1}(n) + (n + j + 1) \, e_{j,k}(n)\) for all \(j, k \in \mathbb{N}\); \(e_{j,k}(n) = \sum_{\ell=0}^{k} \binom{j-k+\ell}{\ell} [j, j-k+\ell] \, (n + 1)^\ell\) for all \(k \le j\); and for all \(j\), \(\sum_{k=0}^{j} e_{j,k}(n) = (n + 2)^{\overline{j}}\) and \(\sum_{k=0}^{j} (-1)^k e_{j,k}(n) = (-1)^j n^{\overline{j}}\).

public theorem_wanted hyperseq_esymm_recurrence_closed_form_row_sums (n : ℕ) :
    (∀ k : ℕ, ((Finset.Icc 1 0).val.map (n + ·)).esymm k = if k = 0 then 1 else 0) ∧
    (∀ j k : ℕ, ((Finset.Icc 1 (j + 1)).val.map (n + ·)).esymm (k + 1) =
      ((Finset.Icc 1 j).val.map (n + ·)).esymm (k + 1) +
        (n + (j + 1)) * ((Finset.Icc 1 j).val.map (n + ·)).esymm k) ∧
    (∀ j k : ℕ, k ≤ j → ((Finset.Icc 1 j).val.map (n + ·)).esymm k =
      ∑ ℓ ∈ Finset.range (k + 1),
        (j - k + ℓ).choose ℓ * Nat.stirlingFirst j (j - k + ℓ) * (n + 1) ^ ℓ) ∧
    (∀ j : ℕ, ∑ k ∈ Finset.range (j + 1), ((Finset.Icc 1 j).val.map (n + ·)).esymm k =
      (n + 2).ascFactorial j) ∧
    ∀ j : ℕ, ∑ k ∈ Finset.range (j + 1),
        (-1 : ℤ) ^ k * (((Finset.Icc 1 j).val.map (n + ·)).esymm k : ℕ) =
      (-1 : ℤ) ^ j * (n.ascFactorial j : ℕ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Proposition 1.

TheoremElementary symmetric functions of the first integers via Stirling numbers#●ready to prove

For \(j, k \in \mathbb{N}\) let \(e_{j,k}\) be the elementary symmetric polynomial of degree \(k\) evaluated at \(1, 2, \dots, j\) (the source's \(e_{j,k}(0)\)), and let \(c(j, i)\) be the unsigned Stirling number of the first kind. Then \(e_{0,k} = 1\) if \(k = 0\) and \(e_{0,k} = 0\) otherwise; for all \(j, k\), \(e_{j+1,k+1} = e_{j,k+1} + (j + 1)\, e_{j,k}\); and for all \(k \le j\),

\[e_{j,k} = \sum_{\ell=0}^{k} \binom{j-k+\ell}{\ell}\, c(j, j-k+\ell) = c(j + 1, j + 1 - k).\]

public theorem_wanted hyperseq_esymm_zero_recurrence_stirling :
    (∀ k : ℕ, ((Finset.Icc 1 0).val).esymm k = if k = 0 then 1 else 0) ∧
    (∀ j k : ℕ, ((Finset.Icc 1 (j + 1)).val).esymm (k + 1) =
      ((Finset.Icc 1 j).val).esymm (k + 1) +
        (j + 1) * ((Finset.Icc 1 j).val).esymm k) ∧
    ∀ j k : ℕ, k ≤ j →
      ((Finset.Icc 1 j).val).esymm k =
          ∑ ℓ ∈ Finset.range (k + 1), (j - k + ℓ).choose ℓ * Nat.stirlingFirst j (j - k + ℓ) ∧
        ((Finset.Icc 1 j).val).esymm k = Nat.stirlingFirst (j + 1) (j + 1 - k)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Corollary 3.

DefinitionParisse's matrix \(B(n)\)#✓fully proved

For an integer \(n\) and \(j, k \in \mathbb{N}\), let \(e_{j,i}(n)\) be the elementary symmetric polynomial of degree \(i\) in \(n + 1, \dots, n + j\). The entry \(b_{j,k}(n)\) of \(B(n)\) is \((-1)^k e_{j,j-k}(n)\) for \(k \le j\) and \(0\) for \(k > j\); it is an integer.

The source also uses this for \(n \in \mathbb{Z}\) (Proposition 3, after Remark 1), which is why \(n\) ranges over the integers.

public def hyperseqB (n : ℤ) (j k : ℕ) : ℤ :=
  if k ≤ j then (-1) ^ k * ((Finset.Icc 1 j).val.map fun i : ℕ => n + i).esymm (j - k) else 0

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Section 2, Equation (2.5).

Used by 8

Used byThe inverse of Parisse's matrix \(B(n)\) · Row one of Parisse's matrix \(B(n)\) · Recurrence, closed form and row sums of Parisse's \(b_{j,k}(n)\) · Row three of Parisse's matrix \(B(1)\) · Parisse's \(b_{j,k}(0)\) and Stirling numbers of the first kind · The inverse of Parisse's matrix \(C(n)\) · Parisse's coefficients at \(n\) from their values at \(-1\) · The product of Parisse's matrices B(n) and C(n)

TheoremRow one of Parisse's matrix \(B(n)\)#✓fully proved

For every integer \(n\), the entries \(b_{j,k}(n)\) of \(B(n)\) satisfy \(b_{1,0}(n) = n + 1\) and \(b_{1,1}(n) = -1\).

public theorem hyperseqB_one (n : ℤ) : hyperseqB n 1 0 = n + 1 ∧ hyperseqB n 1 1 = -1

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Section 2, display of B(n).

Uses 1

Statement usesParisse's matrix \(B(n)\)

TheoremRow three of Parisse's matrix \(B(1)\)#✓fully proved

The entries \(b_{3,0}(1), b_{3,1}(1), b_{3,2}(1), b_{3,3}(1)\) of \(B(1)\) are \(24, -26, 9, -1\).

This matches the source's display of row three of \(B(n)\), \((n + 1)(n + 2)(n + 3), -(3n^2 + 12n + 11), 3n + 6, -1\), at \(n = 1\).

public theorem hyperseqB_row_three :
    (List.range 4).map (hyperseqB 1 3) = [24, -26, 9, -1]

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Section 2, display of B(n).

Uses 1

Statement usesParisse's matrix \(B(n)\)

DefinitionMitrinović's numbers#✓fully proved

For complex numbers \(a\) and \(b\), Mitrinović's numbers \(R^k_j(a, b)\), \(j, k \in \mathbb{N}\) (lower index \(j\), upper index \(k\)), are defined by \(R^k_0(a, b) = 1\) if \(k = 0\) and \(R^k_0(a, b) = 0\) otherwise, and, for all \(j, k\), by \(R^0_{j+1}(a, b) = -(a + b j)\, R^0_j(a, b)\) and \(R^{k+1}_{j+1}(a, b) = R^k_j(a, b) - (a + b j)\, R^{k+1}_j(a, b)\).

With \(R = 0\) at negative indices this is the recurrence (4.2), \(R^k_j(a, b) = R^{k-1}_{j-1}(a, b) - (a - b + b j)\, R^k_{j-1}(a, b)\) for \(j \ge 1\). The start value is the source's Corollary 5 at \(a = 0\) and its solution (4.3) at \(j = 0\) for every \(a\).

public def mitrinovicR (a b : ℂ) : ℕ → ℕ → ℂ
  | 0, k => if k = 0 then 1 else 0
  | j + 1, 0 => -(a + b * j) * mitrinovicR a b j 0
  | j + 1, k + 1 => mitrinovicR a b j k - (a + b * j) * mitrinovicR a b j (k + 1)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Section 4, Equation (4.2).

Used by 3

Used byBinomial expansion of Mitrinović's numbers in the first parameter · Mitrinović's numbers with lower index one · Mitrinović's numbers at \(a = 0\)

TheoremMitrinović's numbers with lower index one#✓fully proved

For all complex numbers \(a, b\), Mitrinović's numbers satisfy \(R^0_1(a, b) = -a\) and \(R^1_1(a, b) = 1\).

public theorem mitrinovicR_one (a b : ℂ) :
    mitrinovicR a b 1 0 = -a ∧ mitrinovicR a b 1 1 = 1

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Section 4, Equation (4.2).

Uses 1

Statement usesMitrinović's numbers

TheoremHypersequences through elementary symmetric polynomials#●ready to prove

Let \(a\) be a sequence of complex numbers and let \(j, n \in \mathbb{N}\). Write \(a^{(r)}_n\) for the hypersequence of generation \(r\) of \(a\), write \(e_{j,k}(n)\) for the elementary symmetric polynomial of degree \(k\) in \(n + 1, \dots, n + j\), and put \(t_i(n) = \sum_{k=0}^{n} k^i a_k\), with \(0^0 = 1\). Then \(j! \, a^{(j+1)}_n = (-1)^j \sum_{k=0}^{j} (-1)^k e_{j,k}(n) \, t_{j-k}(n)\) and \(j! \, a^{(j+1)}_n = \sum_{k=0}^{j} (-1)^k e_{j,j-k}(n) \, t_k(n)\).

public theorem_wanted factorial_mul_hypersequence_eq_sum_esymm (a : ℕ → ℂ) (j n : ℕ) :
    (j.factorial : ℂ) * hypersequence a (j + 1) n =
        (-1) ^ j * ∑ k ∈ Finset.range (j + 1), (-1) ^ k *
          (((Finset.Icc 1 j).val.map (n + ·)).esymm k : ℕ) *
            ∑ i ∈ Finset.range (n + 1), (i : ℂ) ^ (j - k) * a i ∧
      (j.factorial : ℂ) * hypersequence a (j + 1) n =
        ∑ k ∈ Finset.range (j + 1), (-1) ^ k *
          (((Finset.Icc 1 j).val.map (n + ·)).esymm (j - k) : ℕ) *
            ∑ i ∈ Finset.range (n + 1), (i : ℂ) ^ k * a i

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Theorem 1, Equation (2.1).

Uses 1

Statement usesHypersequence

TheoremThe inverse of Parisse's matrix \(C(n)\)#●ready to prove

Let \(n \in \mathbb{N}\). Let \(e_{j,i}(n)\) be the elementary symmetric polynomial of degree \(i\) in \(n + 1, \dots, n + j\), let \(b_{j,k}(n) = (-1)^k e_{j,j-k}(n)\) for \(k \le j\) and \(b_{j,k}(n) = 0\) for \(k > j\), let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k x + y)^\ell\) for complex \(x, y\), and let \(c_{\ell,m}(n) = p_{\ell,m}(1, n + 1) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k + n + 1)^\ell\). Then for all \(j, m \in \mathbb{N}\), with \(\delta_{j,m}\) the Kronecker delta, \(\sum_{k=0}^{j} \frac{b_{j,k}(n)}{j!} \, c_{k,m}(n) = \delta_{j,m}\) and \(\sum_{k=0}^{j} c_{j,k}(n) \, \frac{b_{k,m}(n)}{k!} = \delta_{j,m}\).

In matrix form, with \(B(n) = (b_{j,k}(n))\), \(C(n) = (c_{\ell,m}(n))\) and \(D\) the diagonal matrix of the factorials \(j!\), this says \(C(n)^{-1} = D^{-1} B(n)\); both matrices are lower triangular, so each entry of the two products is the finite sum above.

public theorem_wanted hyperseqC_inv_eq_hyperseqB_div_factorial (n j m : ℕ) :
    ∑ k ∈ Finset.range (j + 1), (hyperseqB n j k : ℂ) / j.factorial *
        alternatingBinomialPowerSum k m 1 (n + 1) = (if j = m then 1 else 0) ∧
      ∑ k ∈ Finset.range (j + 1), alternatingBinomialPowerSum j k 1 (n + 1) *
        ((hyperseqB n k m : ℂ) / k.factorial) = if j = m then 1 else 0

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Theorem 2.

Uses 2

Statement usesAlternating binomial power sum · Parisse's matrix \(B(n)\)

TheoremThe inverse of Parisse's matrix \(B(n)\)#●ready to prove

Let \(n \in \mathbb{N}\). Let \(e_{j,i}(n)\) be the elementary symmetric polynomial of degree \(i\) in \(n + 1, \dots, n + j\), let \(b_{j,k}(n) = (-1)^k e_{j,j-k}(n)\) for \(k \le j\) and \(b_{j,k}(n) = 0\) for \(k > j\), let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k x + y)^\ell\) for complex \(x, y\), and let \(c_{\ell,m}(n) = p_{\ell,m}(1, n + 1) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k + n + 1)^\ell\). Then for all \(j, m \in \mathbb{N}\), with \(\delta_{j,m}\) the Kronecker delta, \(\sum_{k=0}^{j} b_{j,k}(n) \, \frac{c_{k,m}(n)}{m!} = \delta_{j,m}\) and \(\sum_{k=0}^{j} \frac{c_{j,k}(n)}{k!} \, b_{k,m}(n) = \delta_{j,m}\).

In matrix form, with \(B(n) = (b_{j,k}(n))\), \(C(n) = (c_{\ell,m}(n))\) and \(D\) the diagonal matrix of the factorials \(j!\), this says \(B(n)^{-1} = C(n) D^{-1}\).

public theorem_wanted hyperseqB_inv_eq_hyperseqC_div_factorial (n j m : ℕ) :
    ∑ k ∈ Finset.range (j + 1), (hyperseqB n j k : ℂ) *
        (alternatingBinomialPowerSum k m 1 (n + 1) / m.factorial) = (if j = m then 1 else 0) ∧
      ∑ k ∈ Finset.range (j + 1), alternatingBinomialPowerSum j k 1 (n + 1) / k.factorial *
        (hyperseqB n k m : ℂ) = if j = m then 1 else 0

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Corollary 1, Equation (2.9).

Uses 2

Statement usesAlternating binomial power sum · Parisse's matrix \(B(n)\)

TheoremThe product of Parisse's matrices B(n) and C(n)#●ready to prove

For \(n, j, m \in \mathbb{N}\) let \(b_{j,i}(n) = (-1)^i e_{j-i}(n + 1, \dots, n + j)\) for \(i \le j\) be the entries of Parisse's matrix \(B(n)\), where \(e_d\) is the elementary symmetric polynomial of degree \(d\), and let \(c_{i,m}(n) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k + n + 1)^i\) be the entries of \(C(n)\). Then \(\sum_{i=0}^{j} b_{j,i}(n)\, c_{i,m}(n)\) equals \(j!\) if \(j = m\) and \(0\) otherwise.

public theorem_wanted sum_hyperseqB_mul_hyperseqC (n j m : ℕ) :
    ∑ i ∈ Finset.range (j + 1), (hyperseqB n j i : ℂ) * alternatingBinomialPowerSum i m 1 (n + 1) =
      if j = m then (j.factorial : ℂ) else 0

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Corollary 2.

Uses 2

Statement usesAlternating binomial power sum · Parisse's matrix \(B(n)\)

TheoremRecurrence, closed form and row sums of Parisse's \(b_{j,k}(n)\)#●ready to prove

Let \(n \in \mathbb{N}\) and let \(b_{j,k}(n)\) be the entries of Parisse's matrix \(B(n)\). Write \([j, \ell]\) for the unsigned Stirling numbers of the first kind and \(x^{\overline{j}} = x (x + 1) \cdots (x + j - 1)\) for the rising factorial. Then \(b_{0,k}(n) = \delta_{0,k}\) for all \(k\); for all \(j, k \in \mathbb{N}\), \(b_{j+1,0}(n) = (n + j + 1) \, b_{j,0}(n)\) and \(b_{j+1,k+1}(n) = (n + j + 1) \, b_{j,k+1}(n) - b_{j,k}(n)\); \(b_{j,k}(n) = (-1)^k \sum_{\ell=k}^{j} \binom{\ell}{k} [j, \ell] \, (n + 1)^{\ell-k}\) for all \(j, k\) (an empty sum for \(k > j\)); and for all \(j\), \(\sum_{k=0}^{j} b_{j,k}(n) = n^{\overline{j}}\) and \(\sum_{k=0}^{j} (-1)^k b_{j,k}(n) = (n + 2)^{\overline{j}}\).

public theorem_wanted hyperseqB_recurrence_closed_form_row_sums (n : ℕ) :
    (∀ k : ℕ, hyperseqB n 0 k = if k = 0 then 1 else 0) ∧
    (∀ j : ℕ, hyperseqB n (j + 1) 0 = (n + (j + 1)) * hyperseqB n j 0) ∧
    (∀ j k : ℕ, hyperseqB n (j + 1) (k + 1) =
      (n + (j + 1)) * hyperseqB n j (k + 1) - hyperseqB n j k) ∧
    (∀ j k : ℕ, hyperseqB n j k = (-1) ^ k * ∑ ℓ ∈ Finset.Icc k j,
      (ℓ.choose k * Nat.stirlingFirst j ℓ : ℤ) * ((n : ℤ) + 1) ^ (ℓ - k)) ∧
    (∀ j : ℕ, ∑ k ∈ Finset.range (j + 1), hyperseqB n j k = (n.ascFactorial j : ℤ)) ∧
    ∀ j : ℕ, ∑ k ∈ Finset.range (j + 1), (-1) ^ k * hyperseqB n j k =
      ((n + 2).ascFactorial j : ℤ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Proposition 2.

Uses 1

Statement usesParisse's matrix \(B(n)\)

TheoremParisse's \(b_{j,k}(0)\) and Stirling numbers of the first kind#●ready to prove

Let \(b_{j,k}(0)\) be the entries of Parisse's matrix \(B(0)\) and write \([j, \ell]\) for the unsigned Stirling numbers of the first kind. Then \(b_{0,k}(0) = \delta_{0,k}\) for all \(k\); for all \(j, k \in \mathbb{N}\), \(b_{j+1,0}(0) = (j + 1) \, b_{j,0}(0)\) and \(b_{j+1,k+1}(0) = (j + 1) \, b_{j,k+1}(0) - b_{j,k}(0)\); and for all \(j, k \in \mathbb{N}\), \(b_{j,k}(0) = (-1)^k \sum_{\ell=k}^{j} \binom{\ell}{k} [j, \ell] = (-1)^k [j + 1, k + 1]\).

public theorem_wanted hyperseqB_zero_recurrence_stirling :
    (∀ k : ℕ, hyperseqB 0 0 k = if k = 0 then 1 else 0) ∧
    (∀ j : ℕ, hyperseqB 0 (j + 1) 0 = (j + 1) * hyperseqB 0 j 0) ∧
    (∀ j k : ℕ, hyperseqB 0 (j + 1) (k + 1) = (j + 1) * hyperseqB 0 j (k + 1) - hyperseqB 0 j k) ∧
    ∀ j k : ℕ,
      hyperseqB 0 j k = (-1) ^ k * ∑ ℓ ∈ Finset.Icc k j, (ℓ.choose k * Nat.stirlingFirst j ℓ : ℤ) ∧
        hyperseqB 0 j k = (-1) ^ k * Nat.stirlingFirst (j + 1) (k + 1)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Corollary 4.

Uses 1

Statement usesParisse's matrix \(B(n)\)

TheoremParisse's coefficients at \(n\) from their values at \(-1\)#●ready to prove

Let \(n \in \mathbb{Z}\). For \(j, k \in \mathbb{N}\) let \(e_{j,k}(n)\) be the elementary symmetric polynomial of degree \(k\) in \(n + 1, \dots, n + j\), let \(b_{j,k}(n) = (-1)^k e_{j,j-k}(n)\) for \(k \le j\) and \(b_{j,k}(n) = 0\) for \(k > j\), let \(p_{\ell,m}(x, y) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k x + y)^\ell\) for complex \(x, y\), with \(0^0 = 1\), and let \(c_{\ell,m}(n) = p_{\ell,m}(1, n + 1) = \sum_{k=0}^{m} (-1)^k \binom{m}{k} (k + n + 1)^\ell\). Then \(e_{j,k}(n) = \sum_{i=0}^{k} \binom{j - k + i}{i} (n + 1)^i e_{j,k-i}(-1)\) for all \(k \le j\), \(b_{j,k}(n) = \sum_{i=k}^{j} (-1)^{i-k} \binom{i}{k} (n + 1)^{i-k} b_{j,i}(-1)\) for all \(j, k\), and \(c_{\ell,m}(n) = \sum_{i=m}^{\ell} \binom{\ell}{i} (n + 1)^{\ell-i} c_{i,m}(-1)\) for all \(\ell, m \in \mathbb{N}\).

The first identity is stated only for \(k \le j\); for \(k > j\) the source's upper index \(j - k + i\) of the binomial coefficient can be negative.

public theorem_wanted hyperseq_entries_eq_sum_at_neg_one (n : ℤ) :
    (∀ j k : ℕ, k ≤ j → ((Finset.Icc 1 j).val.map fun i : ℕ => n + i).esymm k =
      ∑ i ∈ Finset.range (k + 1), ((j - k + i).choose i : ℤ) * (n + 1) ^ i *
        ((Finset.Icc 1 j).val.map fun i : ℕ => (-1 : ℤ) + i).esymm (k - i)) ∧
    (∀ j k : ℕ, hyperseqB n j k =
      ∑ i ∈ Finset.Icc k j, (-1) ^ (i - k) * (i.choose k : ℤ) * (n + 1) ^ (i - k) *
        hyperseqB (-1) j i) ∧
    ∀ ℓ m : ℕ, alternatingBinomialPowerSum ℓ m 1 (n + 1) =
      ∑ i ∈ Finset.Icc m ℓ, (ℓ.choose i : ℂ) * ((n : ℂ) + 1) ^ (ℓ - i) *
        alternatingBinomialPowerSum i m 1 0

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Proposition 3.

Uses 2

Statement usesAlternating binomial power sum · Parisse's matrix \(B(n)\)

TheoremMitrinović's numbers at \(a = 0\)#●ready to prove

For every complex number \(b\), Mitrinović's numbers \(R^k_j(0, b)\) satisfy the following. First, for every \(k \in \mathbb{N}\), \(R^k_0(0, b) = 1\) if \(k = 0\) and \(R^k_0(0, b) = 0\) otherwise. Second, for all \(j, k \in \mathbb{N}\), \(R^{k+1}_{j+1}(0, b) = R^k_j(0, b) + (b - b(j + 1))\, R^{k+1}_j(0, b)\). Third, for all \(j, k \in \mathbb{N}\), \(R^k_j(0, b) = (-b)^{j-k} c(j, k)\), where \(c(j, k)\) is the unsigned Stirling number of the first kind, which is \(0\) for \(k > j\), and the exponent \(j - k\) is read as \(0\) when \(k > j\).

The source prints the last factor of the recurrence as \(R^k_{j-1}(a, b)\); it is \(R^k_{j-1}(0, b)\), the case \(a = 0\) of (4.2). The source's hypothesis \(b \ne 0\) is dropped: at \(b = 0\) both sides of the closed form are \(\delta_{j,k}\).

public theorem_wanted mitrinovicR_zero_eq (b : ℂ) :
    (∀ k : ℕ, mitrinovicR 0 b 0 k = if k = 0 then 1 else 0) ∧
    (∀ j k : ℕ, mitrinovicR 0 b (j + 1) (k + 1) =
      mitrinovicR 0 b j k + (b - b * (j + 1)) * mitrinovicR 0 b j (k + 1)) ∧
    ∀ j k : ℕ, mitrinovicR 0 b j k = (-b) ^ (j - k) * Nat.stirlingFirst j k

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Corollary 5.

Uses 1

Statement usesMitrinović's numbers

TheoremBinomial expansion of Mitrinović's numbers in the first parameter#●ready to prove

For all complex numbers \(a, b\) and all \(j, k \in \mathbb{N}\), Mitrinović's numbers satisfy

\[R^k_j(a, b) = \sum_{\ell=0}^{j-k} (-1)^\ell \binom{k+\ell}{\ell} a^\ell R^{k+\ell}_j(0, b),\]

where the upper limit \(j - k\) is read as \(0\) when \(k > j\) (both sides are then \(0\)).

The source's hypothesis \(b \ne 0\) is not needed: the identity also holds at \(b = 0\).

public theorem_wanted mitrinovicR_eq_sum_mitrinovicR_zero (a b : ℂ) (j k : ℕ) :
    mitrinovicR a b j k =
      ∑ ℓ ∈ Finset.range (j - k + 1), (-1) ^ ℓ * ((k + ℓ).choose ℓ : ℂ) * a ^ ℓ *
        mitrinovicR 0 b j (k + ℓ)

Sources

• Daniele Parisse, On Hypersequences of an Arbitrary Sequence and Their Weighted Sums II, INTEGERS 26 (2026), Article A36, Proposition 4, Equation (4.6).

Uses 1

Statement usesMitrinović's numbers

11 fully proved33 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.