Eulerian polynomials

TheoremEulerian polynomials and the series of (k+1)^n (-p)^k#✓fully proved

Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\), and let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\). For every natural number \(n\) and every complex number \(p\) with \(|p| < 1\), we have \(p + 1 \ne 0\), the series \(\sum_{k \ge 0} (k+1)^n (-p)^k\) is summable, and \(\Psi_n(p)/(p+1)^{n+1} = \sum_{k=0}^{\infty} (k+1)^n (-p)^k\).

theorem ramanujan_part1_ch5_entry4 (n : ℕ) (p : ℂ) (hp : ‖p‖ < 1) :
    p + 1 ≠ 0 ∧
      Summable (chapter5Entry4Term n p) ∧
      chapter5Psi n p / (p + 1) ^ (n + 1) =
        ∑' k : ℕ, chapter5Entry4Term n p k

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5, Entry 4, p. 113.

TheoremTwo finite expansions of the Eulerian polynomials#✓fully proved

Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\), and let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\). For every integer \(n \ge 1\) and every complex number \(p \ne -1\), we have \(p + 1 \ne 0\), \(\Psi_0(p) = 1\), \((-1)^{n+1} p \, \Psi_n(p)/(p+1)^n = \sum_{k=0}^{n} (-1)^k \binom{n}{k} \Psi_k(p)/(p+1)^k\), and \(\Psi_n(p) = \sum_{j=0}^{n-1} (-1)^j \binom{n}{j+1} (p+1)^j \Psi_{n-j-1}(p)\).

theorem ramanujan_part1_ch5_entry5_eulerianexplicit (n : ℕ) (p : ℂ)
    (hn : 1 ≤ n) (hp : p ≠ -1) :
    p + 1 ≠ 0 ∧
      chapter5Psi 0 p = 1 ∧
      (-1 : ℂ) ^ (n + 1) * p * chapter5Psi n p / (p + 1) ^ n =
        ∑ k ∈ range (n + 1), chapter5Entry5Formula51Term n p k ∧
      chapter5Psi n p =
        ∑ j ∈ range n, chapter5Entry5Formula52Term n p j

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5, Entry 5, formulas (5.1) and (5.2).

TheoremNo zeros of e^z + 1 in the disc of radius pi#✓fully proved

For every complex number \(z\) with \(|z| < \pi\), we have \(e^z + 1 \ne 0\).

theorem chapter5Entry8_exp_add_one_ne (z : ℂ) (hz : ‖z‖ < Real.pi) :
    Complex.exp z + 1 ≠ 0

Used by 1

Used byEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)

TheoremEulerian polynomials at p = -1#✓fully proved

Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\), and let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\). For every natural number \(n\), \(\Psi_n(-1) = n!\).

theorem chapter5Entry8_psi_neg_one (n : ℕ) :
    chapter5Psi n (-1 : ℂ) = (n.factorial : ℂ)

Used by 1

Used byEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)

TheoremEulerian polynomials at p = 1 in terms of Bernoulli numbers#✓fully proved

Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\); let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\), and let \(B_m\) be the Bernoulli numbers. For every integer \(n \ge 1\), \(\Psi_n(1) = 2^{n+1}(2^{n+1} - 1)B_{n+1}/(n+1)\).

theorem chapter5Entry8_psi_one (n : ℕ) (hn : 1 ≤ n) :
    chapter5Psi n (1 : ℂ) =
      (2 : ℂ) ^ (n + 1) * ((2 : ℂ) ^ (n + 1) - 1) *
        (bernoulli (n + 1) : ℂ) / (n + 1 : ℂ)

Used by 1

Used byEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)

TheoremBernoulli-number expansion of 1/(e^z + 1) in the disc of radius pi#✓fully proved

Let \(B_m\) be the Bernoulli numbers, with \(B_1 = -\tfrac{1}{2}\). For every complex number \(z\) with \(|z| < \pi\), the series \(\sum_{j \ge 0} (1 - 2^{j+1}) B_{j+1} z^j/(j+1)!\) is summable with sum \(1/(e^z + 1)\).

theorem chapter5Entry8_hasSum_bernoulli (z : ℂ) (hz : ‖z‖ < Real.pi) :
    HasSum (chapter5Entry8BernoulliTerm z)
      (1 / (Complex.exp z + 1))

Used by 1

Used byEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)

TheoremEulerian-polynomial expansion of 1/(e^z + 1) in the disc of radius pi#✓fully proved

Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\), and let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\). For every complex number \(z\) with \(|z| < \pi\), the series \(\sum_{m \ge 0} (-1)^m \Psi_m(1) z^m/(2^{m+1} m!)\) is summable with sum \(1/(e^z + 1)\).

theorem chapter5Entry8_hasSum_psi (z : ℂ) (hz : ‖z‖ < Real.pi) :
    HasSum (chapter5Entry8PsiTerm z)
      (1 / (Complex.exp z + 1))

Used by 1

Used byEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)

TheoremEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)#✓fully proved

Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\); let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\), and let \(B_m\) be the Bernoulli numbers, with \(B_1 = -\tfrac{1}{2}\). For every integer \(n \ge 1\) and every complex number \(z\) with \(|z| < \pi\), we have \(e^z + 1 \ne 0\), \(\Psi_n(-1) = n!\), \(\Psi_n(1) = 2^{n+1}(2^{n+1} - 1)B_{n+1}/(n+1)\), the series \(\sum_{j \ge 0} (1 - 2^{j+1}) B_{j+1} z^j/(j+1)!\) is summable with sum \(1/(e^z + 1)\), and the series \(\sum_{m \ge 0} (-1)^m \Psi_m(1) z^m/(2^{m+1} m!)\) is summable with sum \(1/(e^z + 1)\).

theorem ramanujan_part1_ch5_entry8_eulerianformula (n : ℕ) (z : ℂ)
    (hn : 1 ≤ n) (hz : ‖z‖ < Real.pi) :
    Complex.exp z + 1 ≠ 0 ∧
      chapter5Psi n (-1 : ℂ) = (n.factorial : ℂ) ∧
      chapter5Psi n (1 : ℂ) =
        (2 : ℂ) ^ (n + 1) * ((2 : ℂ) ^ (n + 1) - 1) *
          (bernoulli (n + 1) : ℂ) / (n + 1 : ℂ) ∧
      HasSum (chapter5Entry8BernoulliTerm z)
        (1 / (Complex.exp z + 1)) ∧
      HasSum (chapter5Entry8PsiTerm z)
        (1 / (Complex.exp z + 1))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5, Entry 8.

Uses 5 · Used by 1

Proof usesNo zeros of e^z + 1 in the disc of radius pi · Bernoulli-number expansion of 1/(e^z + 1) in the disc of radius pi · Eulerian-polynomial expansion of 1/(e^z + 1) in the disc of radius pi · Eulerian polynomials at p = -1 · Eulerian polynomials at p = 1 in terms of Bernoulli numbers

Used byEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1), under the old Entry 3 label

TheoremEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1), under the old Entry 3 label#✓fully proved

Eulerian polynomials at 1 and -1 and two series for 1/(e^z + 1), under the old Entry 3 label. Let \(A(n,k)\) be the Eulerian numbers, given by \(A(0,0) = 1\), \(A(0,k) = 0\) for \(k \ge 1\) and \(A(n+1,k) = (k+1)A(n,k) + (n+1-k)A(n,k-1)\), where the last term is \(0\) when \(k = 0\); let \(\Psi_0(p) = 1\) and \(\Psi_n(p) = \sum_{k=0}^{n-1} A(n,k)(-p)^k\) for \(n \ge 1\), and let \(B_m\) be the Bernoulli numbers, with \(B_1 = -\tfrac{1}{2}\). For every integer \(n \ge 1\) and every complex number \(z\) with \(|z| < \pi\), we have \(e^z + 1 \ne 0\), \(\Psi_n(-1) = n!\), \(\Psi_n(1) = 2^{n+1}(2^{n+1} - 1)B_{n+1}/(n+1)\), the series \(\sum_{j \ge 0} (1 - 2^{j+1}) B_{j+1} z^j/(j+1)!\) is summable with sum \(1/(e^z + 1)\), and the series \(\sum_{m \ge 0} (-1)^m \Psi_m(1) z^m/(2^{m+1} m!)\) is summable with sum \(1/(e^z + 1)\).

theorem ramanujan_part1_ch5_entry3_eulerianformula (n : ℕ) (z : ℂ)
    (hn : 1 ≤ n) (hz : ‖z‖ < Real.pi) :
    Complex.exp z + 1 ≠ 0 ∧
      chapter5Psi n (-1 : ℂ) = (n.factorial : ℂ) ∧
      chapter5Psi n (1 : ℂ) =
        (2 : ℂ) ^ (n + 1) * ((2 : ℂ) ^ (n + 1) - 1) *
          (bernoulli (n + 1) : ℂ) / (n + 1 : ℂ) ∧
      HasSum (chapter5Entry8BernoulliTerm z)
        (1 / (Complex.exp z + 1)) ∧
      HasSum (chapter5Entry8PsiTerm z)
        (1 / (Complex.exp z + 1))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 5, Entry 8.

Uses 1

Proof usesEulerian polynomials at 1 and -1 and two series for 1/(e^z + 1)

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.