Potential polynomials

TheoremHoward's formula for the series \(\sum_{k \ge 0} 2x^k/(k+2)!\)#✓fully proved

Let \(n\) be a natural number, let

\[h(x) = \sum_{k \ge 0} \frac{2}{(k+2)!}\, x^k \in \mathbb{Q}[[x]],\]

let \(h^{-1}\) be its inverse in \(\mathbb{Q}[[x]]\), and write \([x^n]\, f\) for the coefficient of \(x^n\) in a power series \(f\). Let \(G_n \in \mathbb{Q}[X]\) be a polynomial of degree at most \(n\) such that \(G_n(m) = n!\, [x^n]\, (h^{-1})^m\) for every natural number \(m \le n\). Then

\[G_n(X) = \sum_{i=0}^{n} (-1)^i\, 2^i\, \frac{n!\, i!}{(n+2i)!} \cdot \frac{X(X+1)\cdots(X+i-1)}{i!} \cdot \frac{(X+n)(X+n-1)\cdots(X+i+1)}{(n-i)!} \cdot B_{n+2i,\,i}(0, 1, 1, \dots),\]

where empty products equal \(1\) and \(B_{n+2i,\,i}(0, 1, 1, \dots)\) is the partial Bell polynomial evaluated at the sequence whose first term is \(0\) and whose other terms are all \(1\).

MetaMathlibExt.howard_potentialPolynomial_rTwo_eq_partialBell · 16 lines

theorem howard_potentialPolynomial_rTwo_eq_partialBell
  (G : ℕ → Polynomial Rat) (n : ℕ)
  (hdeg : (G n).natDegree ≤ n)
  (heval : ∀ m : ℕ, m ≤ n →
    (G n).eval (↑m : Rat) = (n.factorial : Rat) *
      PowerSeries.coeff n
        ((PowerSeries.inv (PowerSeries.mk (fun k => (2 : Rat) /
          (((k + 2).factorial : Rat))))) ^ m)) :
  G n = Finset.sum (Finset.range (n + 1)) (fun i =>
    Polynomial.C (((-1 : Rat) ^ i) * ((2 : Rat) ^ i) *
      (((n.factorial : Rat) * (i.factorial : Rat)) / (((n + 2 * i).factorial : Rat)))) *
    ((ascPochhammer Rat i) * Polynomial.C (((i.factorial : Rat))⁻¹)) *
    (((descPochhammer Rat (n - i)).comp (Polynomial.X + Polynomial.C (n : Rat))) *
      Polynomial.C ((((n - i).factorial : Rat))⁻¹)) *
    Polynomial.C (MetaMathlibExt.partialBellPolynomial (n + 2 * i) i
      (fun j => if 2 ≤ j then (1 : Rat) else 0)))

Sources

• G. Nemes, Journal of Integer Sequences 13 (2010), https://cs.uwaterloo.ca/journals/JIS/VOL13/Nemes/nemes2.tex, lines 120-133 (generic) and 166-173 (specialization).

Uses 1

Statement usesPartial Bell polynomial

TheoremHoward's formula for potential polynomials#✓fully proved

Let \(K\) be a field of characteristic zero, let \(r \ge 1\) and \(n\) be natural numbers, and let \(a_0, a_1, a_2, \dots\) be a sequence in \(K\) with \(a_r \ne 0\). Let \(g\) be the formal power series

\[g(x) = \sum_{k \ge 0} \frac{r!\, a_{r+k}}{a_r\, (r+k)!}\, x^k,\]

let \(g^{-1}\) be its inverse in \(K[[x]]\), and write \([x^n]\, f\) for the coefficient of \(x^n\) in a power series \(f\). Let \(P \in K[X]\) be a polynomial of degree at most \(n\) such that \(P(m) = n!\, [x^n]\, (g^{-1})^m\) for every natural number \(m \le n\). Then

\[P(X) = \sum_{i=0}^{n} (-1)^i \left(\frac{r!}{a_r}\right)^i \frac{n!\, i!}{(n+ri)!} \cdot \frac{X(X+1)\cdots(X+i-1)}{i!} \cdot \frac{(X+n)(X+n-1)\cdots(X+i+1)}{(n-i)!} \cdot B_{n+ri,\,i}(\tilde a),\]

where empty products equal \(1\), \(B_{n+ri,\,i}\) is the partial Bell polynomial, and \(\tilde a\) is the sequence with \(\tilde a_j = a_j\) for \(j \ge r\) and \(\tilde a_j = 0\) for \(j < r\).

MetaMathlibExt.howard_potentialPolynomial_eq_partialBell · 18 lines

theorem howard_potentialPolynomial_eq_partialBell
  {K : Type*} [Field K] [CharZero K]
  (r n : ℕ) (hr : 1 ≤ r) (a : ℕ → K) (har : a r ≠ 0)
  (P : Polynomial K)
  (hdeg : P.natDegree ≤ n)
  (heval : ∀ m : ℕ, m ≤ n →
    P.eval (↑m : K) = (n.factorial : K) *
      PowerSeries.coeff n
        ((PowerSeries.inv (PowerSeries.mk (fun k => (r.factorial : K) * a (r + k) /
          (a r * ((r + k).factorial : K))))) ^ m)) :
  P = Finset.sum (Finset.range (n + 1)) (fun i =>
    Polynomial.C (((-1 : K) ^ i) * (((r.factorial : K) / a r) ^ i) *
      (((n.factorial : K) * (i.factorial : K)) / (((n + r * i).factorial : K)))) *
    ((ascPochhammer K i) * Polynomial.C (((i.factorial : K))⁻¹)) *
    (((descPochhammer K (n - i)).comp (Polynomial.X + Polynomial.C (n : K))) *
      Polynomial.C ((((n - i).factorial : K))⁻¹)) *
    Polynomial.C (MetaMathlibExt.partialBellPolynomial (n + r * i) i
      (fun j => if r ≤ j then a j else 0)))

Sources

• G. Nemes, Journal of Integer Sequences 13 (2010), https://cs.uwaterloo.ca/journals/JIS/VOL13/Nemes/nemes2.tex, lines 120-133 (generic) and 166-173 (specialization).

Uses 1

Statement usesPartial Bell polynomial

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.