Binomial transforms

TheoremExponential generating function of the binomial transform#✓fully proved

Let \((a_n)_{n \ge 0}\) and \((b_n)_{n \ge 0}\) be real sequences with \(b_n = \sum_{k=0}^{n} \binom{n}{k} a_k\) for every \(n\), and let \(A : \mathbb{R} \to \mathbb{R}\) be any function. For every real number \(t\), if the series \(\sum_{n \ge 0} a_n t^n / n!\) converges absolutely with sum \(A(t)\), then the series \(\sum_{n \ge 0} b_n t^n / n!\) converges absolutely with sum \(e^t A(t)\).

The formulation is pointwise: convergence of the exponential generating function of \(a\) is assumed only at the point \(t\) under consideration.

theorem exponentialGeneratingFunction_binomialTransform
    (a b : ℕ → ℝ)
    (A : ℝ → ℝ)
    (hbinomial : ∀ n : ℕ,
      b n = ∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) * a k) :
    ∀ t : ℝ, HasSum (fun n : ℕ => a n * t ^ n / n.factorial) (A t) →
      HasSum (fun n : ℕ => b n * t ^ n / n.factorial)
        (Real.exp t * A t)
Sources
  • Ayhan Dil, Veli Kurt, and Mehmet Cenkci, Algorithms for Bernoulli and Related Polynomials, Journal of Integer Sequences 10 (2007), Article 07.5.4, https://cs.uwaterloo.ca/journals/JIS/VOL10/Dil/dil11.tex, Proposition prop2 (proof attributed to Seidel), lines 221-233; the binomial-transform relation a_0^n = Σᵢ C(n,i) a_i^0 is equation (8)/(9), lines 188-199.

DefinitionFalling k-binomial transform#✓fully proved

For an integer \(k\) and an integer sequence \((a_i)_{i \ge 0}\), the falling \(k\)-binomial transform of \(a\) is the integer sequence \((b_n)_{n \ge 0}\) given by

\[b_n = \sum_{i=0}^{n} \binom{n}{i} k^{n-i} a_i.\]
def fallingKBinomialTransform (k : ℤ) (a : ℕ → ℤ) (n : ℕ) : ℤ :=
  ∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * k ^ (n - i) * a i
Used by 2
Used byBinomial transform · The k-fold binomial transform is the falling k-binomial transform

DefinitionBinomial transform#✓fully proved

The binomial transform of an integer sequence \((a_i)_{i \ge 0}\) is the falling k-binomial transform of \(a\) with \(k = 1\), the sequence whose \(n\)-th term is \(\sum_{i=0}^{n} \binom{n}{i} 1^{n-i} a_i\).

def binomialTransform (a : ℕ → ℤ) (n : ℕ) : ℤ :=
  fallingKBinomialTransform 1 a n
Uses 1 · Used by 3
Statement usesFalling k-binomial transform
Used byLayman's theorem: the binomial transform preserves the Hankel transform · Binomial transform as a binomial sum · Multiple binomial transform

TheoremBinomial transform as a binomial sum#✓fully proved

For every integer sequence \((a_i)_{i \ge 0}\) and every \(n \in \mathbb{N}\), the \(n\)-th term of the binomial transform of \(a\) equals \(\sum_{i=0}^{n} \binom{n}{i} a_i\).

theorem binomialTransform_eq_sum (a : ℕ → ℤ) (n : ℕ) :
    binomialTransform a n =
      ∑ i ∈ Finset.range (n + 1), (Nat.choose n i : ℤ) * a i
Uses 1 · Used by 1
Statement usesBinomial transform
Used byLayman's theorem: the binomial transform preserves the Hankel transform

DefinitionMultiple binomial transform#✓fully proved

The binomial transform sends an integer sequence \((a_i)_{i \ge 0}\) to the sequence \((b_n)_{n \ge 0}\) given by \(b_n = \sum_{i=0}^{n} \binom{n}{i} a_i\). For a natural number \(r\), the \(r\)-fold binomial transform of \(a\) is obtained by applying the binomial transform \(r\) times in succession; the \(0\)-fold transform of \(a\) is \(a\) itself.

Concept jis_term_c157679dc9eb88c4ba264101; source statements jis_565fc7c3315ad99b5942cc67 and jis_a569298bba80b28850af1658.

public def multipleBinomialTransform : ℕ → (ℕ → ℤ) → ℕ → ℤ
  | 0, a => a
  | n + 1, a => binomialTransform (multipleBinomialTransform n a)
Sources

-

Uses 1 · Used by 1
Statement usesBinomial transform
Used byThe k-fold binomial transform is the falling k-binomial transform

TheoremThe k-fold binomial transform is the falling k-binomial transform#✓fully proved

For every integer sequence \(a\) and every integer \(k\): if \(k \ge 0\), applying the binomial transform \(k\) times to \(a\) gives the falling \(k\)-binomial transform of \(a\); if \(k < 0\), applying the inverse binomial transform (the falling \((-1)\)-binomial transform) \(-k\) times to \(a\) gives the falling \(k\)-binomial transform of \(a\). In both cases the equality is one of integer sequences.

theorem falling_equiv
    (a : ℕ → ℤ) (k : ℤ) :
    (if 0 ≤ k then multipleBinomialTransform k.toNat a
      else Nat.iterate (fallingKBinomialTransform (-1)) (-k).toNat a) =
      fallingKBinomialTransform k a
Sources
Uses 2
Statement usesFalling k-binomial transform · Multiple binomial transform

TheoremGenerating function of the binomial transform over a field#✓fully proved

Let \(K\) be a field and let \(a : \mathbb{N} \to K\) be a sequence with ordinary generating function \(A(X) = \sum_n a_n X^n \in K[[X]]\). Then the ordinary generating function of the binomial transform \(n \mapsto \sum_{k=0}^{n} \binom{n}{k} a_k\) of \(a\) equals \((1 - X)^{-1} \cdot A\big(X (1 - X)^{-1}\big)\) in \(K[[X]]\), where \(A\big(X (1 - X)^{-1}\big)\) is the power series obtained by substituting \(X (1 - X)^{-1}\) for \(X\) in \(A\).

theorem mk_sum_choose_mul_eq_inv_one_sub_mul_subst {K : Type*} [Field K]
    (a : ℕ → K) :
    PowerSeries.mk
        (fun n : ℕ =>
          ∑ k ∈ Finset.range (n + 1), (n.choose k : K) * a k) =
      (1 - (PowerSeries.X : PowerSeries K))⁻¹ *
        (PowerSeries.mk a).subst
          ((PowerSeries.X : PowerSeries K) * (1 - PowerSeries.X)⁻¹)
Used by 1
Used byOrdinary generating function of the binomial transform

TheoremOrdinary generating function of the binomial transform#✓fully proved

Let \(a : \mathbb{N} \to \mathbb{R}\) be a real sequence with ordinary generating function \(A(X) = \sum_n a_n X^n \in \mathbb{R}[[X]]\). Then the ordinary generating function of the binomial transform \(n \mapsto \sum_{k=0}^{n} \binom{n}{k} a_k\) of \(a\) equals \((1 - X)^{-1} \cdot A\big(X (1 - X)^{-1}\big)\) in \(\mathbb{R}[[X]]\), where \(A\big(X (1 - X)^{-1}\big)\) is the power series obtained by substituting \(X (1 - X)^{-1}\) for \(X\) in \(A\).

theorem ordinary_generating_function_binomial_transform
    (a : ℕ → ℝ) :
    PowerSeries.mk
        (fun n : ℕ =>
          ∑ k ∈ Finset.range (n + 1), (n.choose k : ℝ) * a k) =
      (1 - (PowerSeries.X : PowerSeries ℝ))⁻¹ *
        (PowerSeries.mk a).subst
          ((PowerSeries.X : PowerSeries ℝ) * (1 - PowerSeries.X)⁻¹)
Sources
  • Ayhan Dil, Veli Kurt, and Mehmet Cenkci, "Algorithms for Bernoulli and Related Polynomials," Journal of Integer Sequences 10 (2007), Article 07.5.4, Proposition, lines 205–218 (proof attributed to Euler there). https://cs.uwaterloo.ca/journals/JIS/VOL10/Dil/dil11.tex It is the case K = ℝ of mk_sum_choose_mul_eq_inv_one_sub_mul_subst.
Uses 1
Proof usesGenerating function of the binomial transform over a field
8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.