Median Euler numbers

DefinitionThe list of the first Euler coefficients#✓fully proved

Let \(\varepsilon_N\) be \(1\) if \(N\) is odd and \(0\) if \(N\) is even. For each natural number \(n\), this is the list \([c_0, c_1, \dots, c_n]\) of integers with \(c_0 = 1\) and, for \(1 \le N \le n\), \(c_N = \varepsilon_N - \sum_j \binom{N}{j} c_{N-j}\), where the sum runs over the even \(j\) with \(2 \le j \le N\). The Euler coefficient \(E_n\) is its last entry \(c_n\). The list is built one entry at a time, so each step reuses the earlier values.

The recurrence comes from \(\cosh x \cdot (\operatorname{sech} x + \tanh x) = 1 + \sinh x\).

def medianEulerCoefficients : ℕ → List ℤ
  | 0 => [1]
  | n + 1 =>
      let previous := medianEulerCoefficients n
      let N := n + 1
      let sum : ℤ :=
        ∑ j ∈ Finset.filter (fun j => 2 ≤ j ∧ j % 2 = 0) (Finset.range (N + 1)),
          (N.choose j : ℤ) * previous.getD (N - j) 0
      previous ++ [(if N % 2 = 1 then 1 else 0) - sum]

Used by 2

Used byEuler coefficients · Recurrence for the Euler coefficients

DefinitionEuler coefficients#✓fully proved

Let \(\varepsilon_n\) be \(1\) if \(n\) is odd and \(0\) if \(n\) is even. The Euler coefficients \(E_n\) are the integers defined by \(E_0 = 1\) and, for \(n \ge 1\), \(E_n = \varepsilon_n - \sum_j \binom{n}{j} E_{n-j}\), where the sum runs over the even \(j\) with \(2 \le j \le n\).

They are the coefficients in \(\operatorname{sech} x + \tanh x = \sum_{n \ge 0} E_n x^n / n!\): the recurrence compares coefficients in \(\cosh x \cdot (\operatorname{sech} x + \tanh x) = 1 + \sinh x\). The first values are \(1, 1, -1, -2, 5, 16, -61\).

def medianEulerCoeff (n : ℕ) : ℤ :=
  (medianEulerCoefficients n).getD n 0

Uses 1 · Used by 5

Statement usesThe list of the first Euler coefficients

Used byExponential generating function of the Euler coefficients · Recurrence for the Euler coefficients · The zeroth Euler coefficient · Initial row for the median Euler numbers · Median Euler numbers modulo three and five

DefinitionInitial row for the median Euler numbers#✓fully proved

Let \(E_m\) denote the Euler coefficients. This is the integer sequence \((a_m)_{m \ge 0}\) with \(a_0 = 0\) and \(a_m = E_m\) for \(m \ge 1\). It is the initial row of the Euler–Seidel matrix from which the median Euler numbers are read off.

def medianEulerInitialRow : ℕ → ℤ
  | 0 => 0
  | m + 1 => medianEulerCoeff (m + 1)

Uses 1 · Used by 2

Statement usesEuler coefficients

Used byMedian Euler numbers · Median Euler numbers modulo three and five

DefinitionMedian Euler numbers#✓fully proved

Let \(E_m\) denote the Euler coefficients, and let \((a_n^k)\) be the Euler–Seidel matrix of the initial row \(a_0 = 0\), \(a_m = E_m\) for \(m \ge 1\), so that \(a_n^0 = a_n\) and \(a_n^{k+1} = a_n^k + a_{n+1}^k\). The median Euler number \(R_n\) is the natural number \(|a_{n+1}^n|\). Equivalently, \(R_n = \left|\sum_{i=0}^{n} \binom{n}{i} E_{n+1+i}\right|\).

The first values are \(R_0 = 1\), \(R_1 = 3\), \(R_2 = 24\) and \(R_3 = 402\).

def medianEulerNumber (n : ℕ) : ℕ :=
  (eulerSeidelMatrix medianEulerInitialRow (n + 1) n).natAbs

Uses 2 · Used by 1

Statement usesEuler–Seidel matrix · Initial row for the median Euler numbers

Used byMedian Euler numbers modulo three and five

TheoremThe zeroth Euler coefficient#✓fully proved

The Euler coefficient \(E_0\) equals \(1\).

public theorem medianEulerCoeff_zero : medianEulerCoeff 0 = 1

Uses 1 · Used by 2

Statement usesEuler coefficients

Used byExponential generating function of the Euler coefficients · Median Euler numbers modulo three and five

TheoremRecurrence for the Euler coefficients#✓fully proved

Let \(E_m\) denote the Euler coefficients, and let \(\varepsilon_m\) be \(1\) if \(m\) is odd and \(0\) if \(m\) is even. For every natural number \(n\), \(E_{n+1} = \varepsilon_{n+1} - \sum_j \binom{n+1}{j} E_{n+1-j}\), where the sum runs over the even \(j\) with \(2 \le j \le n+1\).

It comes from comparing coefficients in \(\cosh x \cdot (\operatorname{sech} x + \tanh x) = 1 + \sinh x\).

public theorem medianEulerCoeff_succ (n : ℕ) : medianEulerCoeff (n + 1)
    = (if (n + 1) % 2 = 1 then 1 else 0) -
      ∑ j ∈ Finset.filter (fun j => 2 ≤ j ∧ j % 2 = 0) (Finset.range (n + 1 + 1)),
        ((n + 1).choose j : ℤ) * medianEulerCoeff (n + 1 - j)

Uses 2 · Used by 1

Statement usesEuler coefficients

Proof usesThe list of the first Euler coefficients

Used byExponential generating function of the Euler coefficients

TheoremExponential generating function of the Euler coefficients#✓fully proved

Let \(E_n\) denote the Euler coefficients, let \(e^x\) be the exponential series, and let \(e^{-x}\) be the series obtained from it by replacing \(x\) with \(-x\). In the ring \(\mathbb{Q}[[x]]\) of formal power series with rational coefficients, \((e^x + e^{-x}) \sum_{n \ge 0} E_n x^n / n! = 2 + e^x - e^{-x}\).

Since \(e^x + e^{-x} = 2 \cosh x\) and \(2 + e^x - e^{-x} = 2 (1 + \sinh x)\), and \(\cosh x\) is invertible, this says that the exponential generating function of the \(E_n\) is \(\operatorname{sech} x + \tanh x\).

public theorem medianEulerCoeff_egf :
    (PowerSeries.exp ℚ + PowerSeries.rescale (-1) (PowerSeries.exp ℚ)) *
      PowerSeries.mk (fun n => ((medianEulerCoeff n : ℤ) : ℚ) / (n.factorial : ℚ))
    = 2 + PowerSeries.exp ℚ - PowerSeries.rescale (-1) (PowerSeries.exp ℚ)

Uses 3 · Used by 1

Statement usesEuler coefficients

Proof usesRecurrence for the Euler coefficients · The zeroth Euler coefficient

Used byMedian Euler numbers modulo three and five

TheoremMedian Euler numbers modulo three and five#✓fully proved

For every natural number \(n \ge 1\), the median Euler number \(R_n\) is divisible by \(3\), and \(R_n / 3 \equiv 3^{n-1} \pmod 5\).

public theorem medianEulerNumber_div_three_and_modFive {n : ℕ} (hn : 1 ≤ n) :
    3 ∣ medianEulerNumber n ∧ Nat.ModEq 5 (medianEulerNumber n / 3) (3 ^ (n - 1))

Uses 7

Statement usesMedian Euler numbers

Proof usesEuler–Seidel matrix · Closed form of the Euler–Seidel matrix · Euler coefficients · Exponential generating function of the Euler coefficients · The zeroth Euler coefficient · Initial row for the median Euler numbers

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.