Euler numbers

DefinitionEven-index Euler numbers#✓fully proved

The integers \(E_0, E_2, E_4, \dots\) defined recursively by \(E_0 = 1\) and \(E_{2m} = -\sum_{k=0}^{m-1} \binom{2m}{2k} E_{2k}\) for \(m \ge 1\); equivalently, \(\sum_{k=0}^{m} \binom{2m}{2k} E_{2k}\) is \(1\) for \(m = 0\) and \(0\) for \(m \ge 1\). The value at \(n\) is \(E_{2n}\).

The first values are \(E_0 = 1\), \(E_2 = -1\), \(E_4 = 5\), \(E_6 = -61\); the absolute values are the secant numbers.

def chapter5EulerEven (n : ℕ) : ℤ :=
  Nat.strongRec (motive := fun _ => ℤ)
    (fun m previous =>
      if m = 0 then 1
      else -∑ k : Fin m,
        (Nat.choose (2 * m) (2 * k.val) : ℤ) * previous k.val k.isLt) n

Used by 12

Used byAlzer–Richards identity for Euler numbers · Class number congruences for \(\mathbb{Q}(\sqrt{-p})\) · Euler numbers · Binomial recurrence for the even-index Euler numbers · Recursion for the even-index Euler numbers · The initial even-index Euler number · Bernoulli numbers as a convolution of even-index Euler numbers · Dirichlet beta at odd positive integers · Hurwitz zeta at \(3/4\) and odd arguments · Tóth's paperfolding and Thue–Morse series for \(\zeta(2k+1)\) · The \(\pm 1\) paperfolding Dirichlet series at odd integers · A paperfolding Dirichlet series at odd integers

TheoremThe initial even-index Euler number#✓fully proved

\(E_0 = 1\).

theorem chapter5EulerEven_zero : chapter5EulerEven 0 = 1

Uses 1 · Used by 1

Statement usesEven-index Euler numbers

Used byBinomial recurrence for the even-index Euler numbers

TheoremRecursion for the even-index Euler numbers#✓fully proved

For every natural number \(m \ge 1\), \(E_{2m} = -\sum_{k=0}^{m-1} \binom{2m}{2k} E_{2k}\).

theorem chapter5EulerEven_step (m : ℕ) (hm : m ≠ 0) :
    chapter5EulerEven m =
      -∑ k : Fin m, (Nat.choose (2 * m) (2 * k.val) : ℤ) * chapter5EulerEven k.val

Uses 1 · Used by 1

Statement usesEven-index Euler numbers

Used byBinomial recurrence for the even-index Euler numbers

TheoremBinomial recurrence for the even-index Euler numbers#✓fully proved

For every natural number \(m\), \(\sum_{k=0}^{m} \binom{2m}{2k} E_{2k}\) is \(1\) if \(m = 0\) and \(0\) if \(m \ge 1\).

theorem chapter5EulerEven_recurrence (m : ℕ) :
    ∑ k ∈ Finset.range (m + 1),
      ((Nat.choose (2 * m) (2 * k) : ℕ) : ℤ) * chapter5EulerEven k =
      if m = 0 then 1 else 0

Uses 3 · Used by 1

Statement usesEven-index Euler numbers

Proof usesRecursion for the even-index Euler numbers · The initial even-index Euler number

Used byBernoulli numbers as a convolution of even-index Euler numbers

TheoremBernoulli numbers as a convolution of even-index Euler numbers#✓fully proved

For every natural number \(n\), \(2^{2n} (2^{2n} - 1) B_{2n} = 2n \sum_{k=0}^{n-1} \binom{2n-2}{2k} E_{2k} E_{2n-2k-2}\), where \(B_m\) are the Bernoulli numbers and \(E_{2k}\) are the even-index Euler numbers.

theorem ramanujan_part1_ch5_entry10b_euleriansymmetry (n : ℕ) :
    (2 : ℚ) ^ (2 * n) * ((2 : ℚ) ^ (2 * n) - 1) * bernoulli (2 * n) =
      ((2 * n : ℕ) : ℚ) *
        ∑ k ∈ range n,
          (Nat.choose (2 * n - 2) (2 * k) : ℚ) *
            (chapter5EulerEven k : ℚ) *
              (chapter5EulerEven (n - k - 1) : ℚ)

Sources

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

Uses 2

Statement usesEven-index Euler numbers

Proof usesBinomial recurrence for the even-index Euler numbers

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.