Higher-order Euler polynomials

DefinitionEuler polynomials#✓fully proved

Let \(B_m(x)\) denote the \(m\)-th Bernoulli polynomial. For \(n \ge 0\), the Euler polynomial \(E_n(x)\) is the polynomial with rational coefficients \(E_n(x) = \frac{2}{n + 1} \left(B_{n+1}(x) - 2^{n+1} B_{n+1}(x/2)\right)\).

noncomputable def eulerPoly (n : ℕ) : ℚ[X] :=
  (2 / (n + 1 : ℚ)) • (Polynomial.bernoulli (n + 1) -
    (2 : ℚ) ^ (n + 1) •
      (Polynomial.bernoulli (n + 1)).comp (C (1 / 2) * X))

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Section 1 (Euler polynomials).

Used by 7

Used byThe congruence \(\sum_{j=0}^{p} E_j(0) \equiv 3/2 \pmod p\) · Fuel-bounded recurrence for the Euler numbers of order α · Euler polynomials as alternating sums of shifted powers · Double-sum formula for Euler polynomials · Euler polynomials via generalized Stirling polynomials · Recurrence for Euler polynomials of order α · Euler polynomials at (x + 1)/2 via generalized Stirling polynomials

DefinitionGeneralized Stirling polynomial#✓fully proved

For natural numbers \(n\) and \(k\), the generalized Stirling polynomial \(S(n, k, x)\) is the polynomial in \(x\) with rational coefficients

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

noncomputable def genStirlingPoly (n k : ℕ) : ℚ[X] :=
  (1 / (Nat.factorial k : ℚ)) •
    ∑ j ∈ Finset.range (k + 1),
      ((Nat.choose k j : ℚ) * (-1) ^ (k - j)) •
        (X + C (j : ℚ)) ^ n

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Proposition 3.1 (definition).

Used by 3

Used byDouble-sum formula for Euler polynomials · Euler polynomials via generalized Stirling polynomials · Euler polynomials at (x + 1)/2 via generalized Stirling polynomials

DefinitionTaylor coefficients of (2 + 2z)/(2 + 2z + z²)#✓fully proved

The rational numbers \(\alpha_k\), \(k \ge 0\), are defined by \(\alpha_0 = 1\), \(\alpha_1 = 0\) and \(2\alpha_{k+2} + 2\alpha_{k+1} + \alpha_k = 0\) for every \(k \ge 0\). They are the Taylor coefficients of \((2 + 2z)/(2 + 2z + z^2)\) at \(z = 0\).

def eulerAlpha : ℕ → ℚ
  | 0 => 1
  | 1 => 0
  | k + 2 => -eulerAlpha (k + 1) - eulerAlpha k / 2

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Lemma 2.2 (generating function).

Used by 2

Used byEuler polynomials via generalized Stirling polynomials · Euler polynomials at (x + 1)/2 via generalized Stirling polynomials

DefinitionFuel-bounded recurrence for the Euler numbers of order α#✓fully proved

Let \(E_m(x)\) denote the Euler polynomial. For a complex number \(\alpha\), the complex numbers \(a_\alpha(f, n)\), for natural numbers \(f\) (the fuel) and \(n\), are defined by \(a_\alpha(0, n) = 1\), \(a_\alpha(f + 1, 0) = 1\) and \(a_\alpha(f + 1, n + 1) = -\alpha \, a_\alpha(f, n) + \frac{\alpha}{2} \sum_{k=0}^{n} \binom{n}{k} a_\alpha(f, k) \, E_{n-k}(0)\).

Whenever \(n \le f\), \(a_\alpha(f, n)\) equals the Euler number of order \(\alpha\), \(E_n^{(\alpha)}(0)\).

noncomputable def eulerNumGenAux (α : ℂ) : ℕ → ℕ → ℂ
  | 0, _ => 1
  | _ + 1, 0 => 1
  | fuel + 1, n + 1 =>
      -α * eulerNumGenAux α fuel n + (α / 2) *
        ∑ k ∈ Finset.range (n + 1),
          (Nat.choose n k : ℂ) * eulerNumGenAux α fuel k *
            (((eulerPoly (n - k)).eval (0 : ℚ) : ℚ) : ℂ)

Uses 1 · Used by 1

Statement usesEuler polynomials

Used byEuler numbers of order α

DefinitionEuler numbers of order α#✓fully proved

Let \(E_m(x)\) denote the Euler polynomial. For a complex number \(\alpha\), the Euler numbers of order \(\alpha\) are the complex numbers \(E_n^{(\alpha)}(0)\), \(n \ge 0\), defined by \(E_0^{(\alpha)}(0) = 1\) and \(E_{n+1}^{(\alpha)}(0) = -\alpha E_n^{(\alpha)}(0) + \frac{\alpha}{2} \sum_{k=0}^{n} \binom{n}{k} E_k^{(\alpha)}(0) \, E_{n-k}(0)\) for \(n \ge 0\).

This is the coefficient recurrence of the generating function \((2/(e^t + 1))^\alpha\).

noncomputable def eulerNumGen (α : ℂ) (n : ℕ) : ℂ :=
  eulerNumGenAux α n n

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Section 1 (generalized Euler polynomials).

Uses 1 · Used by 1

Statement usesFuel-bounded recurrence for the Euler numbers of order α

Used byEuler polynomials of order α

DefinitionEuler polynomials of order α#✓fully proved

For a complex number \(\alpha\) and \(n \ge 0\), let \(E_k^{(\alpha)}(0)\) denote the Euler numbers of order \(\alpha\). The Euler polynomial of order \(\alpha\) is the complex polynomial \(E_n^{(\alpha)}(x) = \sum_{k=0}^{n} \binom{n}{k} E_k^{(\alpha)}(0) \, x^{n-k}\).

noncomputable def eulerPolyGen (α : ℂ) (n : ℕ) : ℂ[X] :=
  ∑ k ∈ Finset.range (n + 1),
    C ((Nat.choose n k : ℂ) * eulerNumGen α k) * X ^ (n - k)

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Section 1 (generalized Euler polynomials).

Uses 1 · Used by 1

Statement usesEuler numbers of order α

Used byRecurrence for Euler polynomials of order α

TheoremEuler polynomials at (x + 1)/2 via generalized Stirling polynomials#●ready to prove

Let \(E_n(x)\) denote the Euler polynomial, \(\alpha_k\) the Taylor coefficients of \((2 + 2z)/(2 + 2z + z^2)\), and \(S(n, k, x) = \frac{1}{k!} \sum_{j=0}^{k} \binom{k}{j} (-1)^{k-j} (x + j)^n\) the generalized Stirling polynomial. For every \(n \ge 0\), as polynomials in \(x\) with rational coefficients, \(2^n E_n\left(\frac{x + 1}{2}\right) = \sum_{k=0}^{n} k! \, \alpha_k \, S(n, k, x)\).

theorem_wanted eulerPoly_half_eq_sum (n : ℕ) :
    (2 : ℚ) ^ n • (eulerPoly n).comp (C (1 / 2) * (X + 1)) =
      ∑ k ∈ Finset.range (n + 1),
        ((Nat.factorial k : ℚ) * eulerAlpha k) •
          genStirlingPoly n k

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Proposition 3.1.

Uses 3

Statement usesTaylor coefficients of (2 + 2z)/(2 + 2z + z²) · Euler polynomials · Generalized Stirling polynomial

TheoremRecurrence for Euler polynomials of order α#●ready to prove

Let \(E_m(x)\) denote the Euler polynomial and \(E_m^{(\alpha)}(x)\) the Euler polynomial of order \(\alpha\). For every complex number \(\alpha\) and every integer \(n \ge 1\), as polynomials in \(x\), \(E_n^{(\alpha)}(x) = (x - \alpha/2) \, E_{n-1}^{(\alpha)}(x) + \frac{\alpha}{2} \sum_{k=0}^{n-2} \binom{n-1}{k} (-1)^{n-k} E_{n-1-k}(0) \, E_k^{(\alpha)}(x)\), where the sum is empty when \(n = 1\).

theorem_wanted eulerPolyGen_recurrence (α : ℂ) (n : ℕ)
    (hn : 1 ≤ n) :
    eulerPolyGen α n =
      (X - C (α / 2)) * eulerPolyGen α (n - 1) +
        C (α / 2) * ∑ k ∈ Finset.range (n - 1),
          C ((Nat.choose (n - 1) k : ℂ) * (-1) ^ (n - k) *
            (((eulerPoly (n - 1 - k)).eval (0 : ℚ) : ℚ) : ℂ)) *
            eulerPolyGen α k

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Proposition 3.2.

Uses 2

Statement usesEuler polynomials · Euler polynomials of order α

TheoremEuler polynomials as alternating sums of shifted powers#●ready to prove

Let \(E_n(x)\) denote the Euler polynomial. For all natural numbers \(m \ge 2\) and \(n \le 2m + 1\), \(E_n(x) = \sum_{k=0}^{m} \frac{(-1)^k}{2^k} \binom{m+1}{k+1} \sum_{j=0}^{k} \binom{k}{j} \left(x + j - \frac{k+1}{2}\right)^n\) as polynomials in \(x\) with rational coefficients.

theorem_wanted eulerPoly_eq_binomial_average (m n : ℕ)
    (hm : 2 ≤ m) (hn : n ≤ 2 * m + 1) :
    eulerPoly n =
      ∑ k ∈ Finset.range (m + 1),
        ((-1) ^ k * (Nat.choose (m + 1) (k + 1) : ℚ) /
            (2 : ℚ) ^ k) •
          ∑ j ∈ Finset.range (k + 1),
            (Nat.choose k j : ℚ) •
              (X + C ((j : ℚ) - (k + 1 : ℚ) / 2)) ^ n

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Theorem 4.1.

Uses 1

Statement usesEuler polynomials

TheoremEuler polynomials via generalized Stirling polynomials#●ready to prove

Let \(E_n(x)\) denote the Euler polynomial, \(\alpha_k\) the Taylor coefficients of \((2 + 2z)/(2 + 2z + z^2)\), and \(S(n, k, x) = \frac{1}{k!} \sum_{j=0}^{k} \binom{k}{j} (-1)^{k-j} (x + j)^n\) the generalized Stirling polynomial. For every integer \(n \ge 1\), as polynomials in \(x\) with rational coefficients, \(2^n E_n(x) = \sum_{k=0}^{n} k! \, \alpha_k \, S(n, k, 2x - 1)\).

theorem_wanted eulerPoly_eq_sum_genStirling (n : ℕ)
    (hn : 1 ≤ n) :
    (2 : ℚ) ^ n • eulerPoly n =
      ∑ k ∈ Finset.range (n + 1),
        ((Nat.factorial k : ℚ) * eulerAlpha k) •
          (genStirlingPoly n k).comp (C 2 * X - 1)

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Theorem 4.2.

Uses 3

Statement usesTaylor coefficients of (2 + 2z)/(2 + 2z + z²) · Euler polynomials · Generalized Stirling polynomial

TheoremDouble-sum formula for Euler polynomials#●ready to prove

Let \(E_n(x)\) denote the Euler polynomial and \(S(n, k, x) = \frac{1}{k!} \sum_{j=0}^{k} \binom{k}{j} (-1)^{k-j} (x + j)^n\) the generalized Stirling polynomial. For every \(n \ge 0\), as polynomials in \(x\) with rational coefficients, \(2^n E_n(x) = \sum_{\ell=0}^{n} \frac{(-1)^\ell}{\ell + 1} \sum_{k=0}^{n-\ell} \frac{(k + \ell + 1)!}{2^k} \binom{\ell + 1}{k} S(n, k + \ell, 2x - 1)\).

theorem_wanted eulerPoly_eq_double_sum (n : ℕ) :
    (2 : ℚ) ^ n • eulerPoly n =
      ∑ l ∈ Finset.range (n + 1),
        ((-1) ^ l / (l + 1 : ℚ)) •
          ∑ k ∈ Finset.range (n - l + 1),
            ((Nat.factorial (k + l + 1) : ℚ) / (2 : ℚ) ^ k *
                (Nat.choose (l + 1) k : ℚ)) •
              (genStirlingPoly n (k + l)).comp (C 2 * X - 1)

Sources

• Nouara Mokhtari, Rachid Boumahdi, and Farid Bencherif, "Generalizations of Several Explicit Formulas for Euler Polynomials", Theorem 4.3.

Uses 2

Statement usesEuler polynomials · Generalized Stirling polynomial

6 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.