Bernoulli numbers and polynomials

Bernoulli numbers and polynomials, identities, denominators, Kummer congruences, Faulhaber sums, Appell sequences, higher-order and Apostol variants.

DefinitionApostol–Bernoulli numbers#✓fully proved

Let \(\alpha\) be a complex number and let \(\log\) denote the principal branch of the complex logarithm. A sequence \((\beta_k)_{k \ge 0}\) of complex numbers is the sequence of Apostol–Bernoulli numbers \(\beta_k(\alpha)\) when \(\alpha \ne 0\), \(\alpha \ne 1\), and for every complex number \(t\) with \(|t| < |\log \alpha|\) the series \(\sum_{k \ge 0} \beta_k t^k / k!\) converges unconditionally to \(t / (\alpha e^t - 1)\).

public def IsApostolBernoulliSequence (α : ℂ) (β : ℕ → ℂ) : Prop :=
  α ≠ 0 ∧ α ≠ 1 ∧
    ∀ t : ℂ, ‖t‖ < ‖Complex.log α‖ →
      HasSum (fun k : ℕ => β k * t ^ k / (Nat.factorial k : ℂ))
        (t / (α * Complex.exp t - 1))

DefinitionAppell sequence#✓fully proved

Let \(R\) be a field of characteristic zero. A sequence of polynomials \((p_n)_{n \ge 0}\) over \(R\) is an Appell sequence when, for every \(n\), the polynomial \(p_n\) has degree exactly \(n\) (in particular \(p_n \ne 0\)) and the formal derivative of \(p_{n+1}\) equals \((n + 1)\, p_n\).

def IsAppellSequence {R : Type*} [Field R] [CharZero R] (p : ℕ → Polynomial R) : Prop :=
  (∀ n, Polynomial.degree (p n) = ↑n) ∧
    ∀ n, Polynomial.derivative (p (n + 1)) = Polynomial.C ((n + 1 : ℕ) : R) * p n

TheoremFaulhaber-type summation formula for Bernoulli polynomials#✓fully proved

Let \(B_i\) denote the \(i\)-th Bernoulli number, with \(B_1 = -1/2\), and let \(B_j(X) = \sum_{i=0}^{j} \binom{j}{i} B_i X^{j-i} \in \mathbb{Q}[X]\) be the \(j\)-th Bernoulli polynomial. For all natural numbers \(k\) and \(n\), the following identity holds in \(\mathbb{Q}[X]\):

\[\sum_{j=1}^{n} B_k(X + j) = \frac{1}{k+1} \sum_{r=0}^{k} \binom{k+1}{r+1} \left(B_{r+1}(n+1) + (-1)^r B_{r+1}\right) B_{k-r}(X).\]
theorem faulhaber_bernoulli_polynomial_sum
    (k n : ℕ) :
    Finset.sum (Finset.range n) (fun j =>
      (Polynomial.bernoulli k).comp (Polynomial.X + Polynomial.C ((j : ℚ) + 1))) =
      Polynomial.C (1 / ((k : ℚ) + 1)) * Finset.sum (Finset.range (k + 1)) (fun r =>
        Polynomial.C ((Nat.choose (k + 1) (r + 1) : ℚ) *
          ((Polynomial.bernoulli (r + 1)).eval ((n : ℚ) + 1) +
            (-1 : ℚ) ^ r * _root_.bernoulli (r + 1))) *
          Polynomial.bernoulli (k - r))
Sources

TheoremKummer's congruence#✓fully proved

Let \(p\) be a prime, let \(B_j\) denote the \(j\)-th Bernoulli number, with \(B_1 = -1/2\), and let \(t\) be a natural number. Let \(m\) and \(n\) be natural numbers, neither divisible by \(p - 1\), with \(m \equiv n \pmod{(p-1)p^t}\). Then the rational numbers

\[\frac{(1 - p^{m-1}) B_m}{m} \quad \text{and} \quad \frac{(1 - p^{n-1}) B_n}{n}\]

are either equal, or their difference has \(p\)-adic valuation at least \(t + 1\).

In other words, the two numbers agree modulo \(p^{t+1}\); equality is listed as a separate case because the \(p\)-adic valuation of \(0\) is taken to be \(0\).

Proof: We use Voronoi's finite-sum congruence in p-adic norm form, following Ireland--Rosen, Ch. 15 §2, and Washington, Cor. 5.14, back to Kummer's 1851 paper.

public theorem kummer_congruence {p m n t : ℕ} [Fact (Nat.Prime p)]
    (hm_dvd : ¬ (p - 1) ∣ m) (hn_dvd : ¬ (p - 1) ∣ n)
    (hcong : m ≡ n [MOD (p - 1) * p ^ t]) :
    ((1 - (p : ℚ) ^ (m - 1)) * bernoulli m / (m : ℚ)) =
      ((1 - (p : ℚ) ^ (n - 1)) * bernoulli n / (n : ℚ)) ∨
    (t : ℤ) + 1 ≤ padicValRat p
      (((1 - (p : ℚ) ^ (m - 1)) * bernoulli m / (m : ℚ)) -
        ((1 - (p : ℚ) ^ (n - 1)) * bernoulli n / (n : ℚ)))
Sources
  • Ernst Eduard Kummer, "Über eine allgemeine Eigenschaft der rationalen Entwickelungscoefficienten einer bestimmten Gattung analytischer Functionen," Journal für die reine und angewandte Mathematik 41 (1851), 368–372, DOI 10.1515/crll.1851.41.368, https://doi.org/10.1515/crll.1851.41.368.
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.