Stieltjes constants

TheoremStieltjes constants exist, and the zeroth is Euler's constant#✓fully proved

There is exactly one sequence of real numbers \((c_k)_{k \ge 0}\) such that, for every \(k \ge 0\),

\[\sum_{j=1}^{m} \frac{(\log j)^k}{j} - \frac{(\log m)^{k+1}}{k+1} \longrightarrow c_k \quad (m \to \infty),\]

and \(c_0 = \gamma\), where \(\gamma\) is Euler's constant.

theorem ramanujan_part1_ch7_entry13_bernoullipolyadd :
    ∃! c : ℕ → ℝ,
      (∀ k : ℕ, Tendsto (chapter7StieltjesApprox k) atTop (𝓝 (c k))) ∧
        c 0 = Real.eulerMascheroniConstant

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 13.

TheoremLaurent expansion of \(\zeta\) at \(s = 1\)#✓fully proved

Let \((c_k)_{k \ge 0}\) be real numbers such that, for every \(k \ge 0\), \(\sum_{j=1}^{m} (\log j)^k / j - (\log m)^{k+1} / (k+1)\) tends to \(c_k\) as \(m \to \infty\). Then for every complex \(s \ne 1\) the series

\[\sum_{k=0}^{\infty} \frac{(-1)^k c_k}{k!} (s-1)^k\]

converges absolutely, and its sum is \(\zeta(s) - \frac{1}{s-1}\).

theorem ramanujan_part1_ch7_entry13_bernoullirecurrence
    (c : ℕ → ℝ)
    (hc : ∀ k : ℕ,
      Tendsto (chapter7StieltjesApprox k) atTop (𝓝 (c k))) :
    ∀ s : ℂ, s ≠ 1 →
      HasSum (chapter7StieltjesLaurentTerm c s)
        (riemannZeta s - 1 / (s - 1))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 7, Entry 13.

Used by 1

Used byExpansion of \(\sum 1/(n^{s+1} \log n)\) in the Stieltjes constants

TheoremExpansion of \(\sum 1/(n^{s+1} \log n)\) in the Stieltjes constants#✓fully proved

Let \((c_k)_{k \ge 0}\) be real numbers such that, for every \(k \ge 0\), \(\sum_{j=1}^{m} (\log j)^k / j - (\log m)^{k+1} / (k+1)\) tends to \(c_k\) as \(m \to \infty\), and put \(A_k = (-1)^k c_k / k!\). Then the series \(\sum_{n \ge 2} \frac{1}{n^2 \log n}\) and \(\sum_{k \ge 1} \frac{A_k}{k+1}\) converge absolutely, and for every real \(s > 0\) the series \(\sum_{n \ge 2} \frac{1}{n^{s+1} \log n}\) and \(\sum_{k \ge 1} \frac{A_k s^{k+1}}{k+1}\) converge absolutely and

\[\sum_{n=2}^{\infty} \frac{1}{n^{s+1} \log n} = -\log s + C + (1 - \gamma) s - \sum_{k=1}^{\infty} \frac{A_k s^{k+1}}{k+1},\]

where \(\gamma\) is Euler's constant and \(C = \sum_{n \ge 2} \frac{1}{n^2 \log n} - 1 + \gamma + \sum_{k \ge 1} \frac{A_k}{k+1}\).

Proof outline: the limits \(c_k\) are the Stieltjes constants, and \(\zeta(1+s) - 1/s = \sum_{k \ge 0} A_k s^k\). Both sides are differentiated termwise in \(s\), their derivatives agree on \(s > 0\), and the two sides agree at \(s = 1\).

theorem ramanujan_part1_ch7_entry14_bernoulliasymptotic
    (c : ℕ → ℝ)
    (hc : ∀ k : ℕ,
      Tendsto (chapter7StieltjesApprox k) atTop (𝓝 (c k))) :
    Summable (chapter7Entry14Cor2LeftTerm 1) ∧
      Summable (chapter7Entry14Cor2ConstantTerm c) ∧
      ∀ s : ℝ, 0 < s →
        Summable (chapter7Entry14Cor2LeftTerm s) ∧
          Summable (chapter7Entry14Cor2PowerTerm c s) ∧
          (∑' j : ℕ, chapter7Entry14Cor2LeftTerm s j) =
            -Real.log s + chapter7Entry14Cor2Constant c +
              (1 - Real.eulerMascheroniConstant) * s -
                ∑' j : ℕ, chapter7Entry14Cor2PowerTerm c s j

Sources

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

Uses 1

Proof usesLaurent expansion of \(\zeta\) at \(s = 1\)

TheoremTwo definitions of the normalized Stieltjes coefficients agree#✓fully proved

For every real sequence \((c_k)_{k \ge 0}\), the coefficients \(A_k = (-1)^k c_k / k!\) defined for the asymptotic expansion of \(\sum 1/(n(n^x - 1))\) are, by definition, the coefficients \(A_k\) used in the expansion of \(\sum 1/(n^{s+1} \log n)\) in the Stieltjes constants.

theorem chapter7StieltjesA_eq_entry14Bernoulliasymptotic :
    chapter7StieltjesA = Entry14Bernoulliasymptotic.chapter7StieltjesA

TheoremConvergence of \(\sum 1/(n(n^x - 1))\)#✓fully proved

For every real \(x > 0\) the series \(\sum_{n \ge 2} \frac{1}{n(n^x - 1)}\) converges absolutely.

theorem summable_chapter7Entry14Term (x : ℝ) (hx : 0 < x) :
    Summable (chapter7Entry14Term x)

Used by 1

Used byAsymptotic expansion of \(\sum 1/(n(n^x - 1))\) as \(x \to 0^+\)

TheoremTwo definitions of the Stieltjes approximants agree#✓fully proved

For all \(k, m \ge 0\), the approximant \(\sum_{j=1}^{m} (\log j)^k / j - (\log m)^{k+1} / (k+1)\) defined for the asymptotic expansion of \(\sum 1/(n(n^x - 1))\) is, by definition, the approximant used for the existence of the Stieltjes constants.

theorem chapter7StieltjesApprox_eq_entry13Bernoullipolyadd :
    chapter7StieltjesApprox = Entry13Bernoullipolyadd.chapter7StieltjesApprox

TheoremAsymptotic expansion of \(\sum 1/(n(n^x - 1))\) as \(x \to 0^+\)#✓fully proved

Let \(a_0\) be a real number such that \(\sum_{n=2}^{m} \frac{1}{n \log n} - \log \log m\) tends to \(a_0\) as \(m \to \infty\), and let \((c_k)_{k \ge 0}\) be real numbers such that, for every \(k \ge 0\), \(\sum_{j=1}^{m} (\log j)^k / j - (\log m)^{k+1} / (k+1)\) tends to \(c_k\) as \(m \to \infty\). Then for every real \(x > 0\) the series \(F(x) = \sum_{n \ge 2} \frac{1}{n(n^x - 1)}\) converges absolutely, and for every \(N \ge 0\),

\[F(x) = \frac{a_0 - \log x}{x} + \frac{1 - \gamma}{2} + \sum_{k=1}^{N} \frac{B_{2k}\, c_{2k-1}}{(2k)!} x^{2k-1} + O(x^{2N+1}) \quad (x \to 0^+),\]

where \(\gamma\) is Euler's constant and \(B_{2k}\) are the Bernoulli numbers.

Proof: Truncated Laurent expansion of the exponential kernel, an exact partial-sum identity, and a sum-versus-integral error bound, followed by passage to the defining limits.

theorem ramanujan_part1_ch7_entry14_bernoullipolymult
    (a0 : ℝ) (c : ℕ → ℝ)
    (ha0 : Tendsto chapter7Entry14A0Approx atTop (𝓝 a0))
    (hc : ∀ k : ℕ,
      Tendsto (chapter7StieltjesApprox k) atTop (𝓝 (c k))) :
    (∀ x : ℝ, 0 < x → Summable (chapter7Entry14Term x)) ∧
      ∀ N : ℕ,
        IsBigO (nhdsWithin 0 (Set.Ioi 0))
          (fun x : ℝ => chapter7Entry14Sum x - chapter7Entry14Approx a0 c N x)
          (fun x : ℝ => x ^ (2 * N + 1))

Sources

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

Uses 5

Proof usesConvergence of \(\sum 1/(n(n^x - 1))\) · Bound on the derivative of the Laurent remainder of \(1/(e^v - 1)\) · The Laurent remainder of \(1/(e^v - 1)\) is differentiable · Remainder of the Laurent expansion of \(1/(e^v - 1)\) · Bound on the Laurent remainder of \(1/(e^v - 1)\)

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.