Log-convexity of Bell numbers

TheoremTurán-type identity for the Bell numbers#✓fully proved

For every natural number \(n \ge 2\), the Bell numbers \(B_m\) satisfy

\[B_{n-1} B_{n+1} - B_n^2 = \frac{1}{2e^2} \sum_{k=2}^{\infty} \sum_{j=1}^{k-1} \frac{j^{n-1} (k-j)^{n-1}}{j! \, (k-j)!} \, (k-2j)^2,\]

where \(e = \exp(1)\).

Every summand is nonnegative and the summand with \(k = 3\), \(j = 1\) is positive, so the identity refines Engel's inequality \(B_n^2 \le B_{n-1} B_{n+1}\) to a strict inequality.

theorem bell_turan_identity
    (n : ℕ) (hn : 2 ≤ n) :
    (Nat.bell (n - 1) : ℝ) * (Nat.bell (n + 1) : ℝ) -
        (Nat.bell n : ℝ) ^ 2 =
      (1 / (2 * Real.exp 1 ^ 2)) *
        ∑' k : {k : ℕ // 2 ≤ k},
          ∑ j ∈ Finset.Icc 1 (k.1 - 1),
            (((j : ℝ) ^ (n - 1) * ((k.1 - j : ℕ) : ℝ) ^ (n - 1)) /
                ((Nat.factorial j : ℝ) * (Nat.factorial (k.1 - j) : ℝ))) *
              ((k.1 : ℝ) - 2 * (j : ℝ)) ^ 2
Sources
Used by 1
Used byEngel's inequality for Bell numbers

TheoremEngel's inequality for Bell numbers#✓fully proved

For every integer \(n \ge 1\), the Bell numbers satisfy \(B_n^2 \le B_{n-1} B_{n+1}\), where \(B_n\) is the number of partitions of an \(n\)-element set.

This non-strict inequality is Eq. (E2) of Horst Alzer, "On Engel's Inequality for Bell Numbers," Journal of Integer Sequences 22 (2019); Alzer's strict refinement is a different result.

theorem engel_bell_log_convexity (n : ℕ) (hn : 1 ≤ n) :
    (Nat.bell n) ^ 2 ≤ Nat.bell (n - 1) * Nat.bell (n + 1)
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL22/Alzer/alzer6.tex, lines 79--104, where B_n is defined as the Bell number and Eq. (E2) states B_n^2 ≤ B_{n-1} B_{n+1} for every integer n ≥ 1. The source attributes this inequality to K. Engel, "On the average rank of an element in a filter of the partition lattice," J. Combin. Theory Ser. A 65 (1994), 67--78.
Uses 1
Proof usesTurán-type identity for the Bell numbers
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.