Touchard polynomials and generalized Bell series

TheoremAbsolute convergence of Ramanujan's Bell-type series (Entry 4)#✓fully proved

For every complex number \(x\) and every natural number \(n\), the series \(\sum_{j=0}^{\infty} \frac{(j+1)^n x^{j+1}}{j!}\) converges absolutely.

theorem ramanujan_part1_ch3_entry4_inner_summable (x : ℂ) (n : ℕ) :
    Summable (fun j : ℕ => ‖((j + 1 : ℂ) ^ n * x ^ (j + 1) / (Nat.factorial j : ℂ))‖)

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 4, formula (4.1), printed pp. 47--48 / PDF pp. 57--58.

Used by 1

Used byExponential generating function of Ramanujan's Bell-type series (Entry 4)

DefinitionRamanujan's generalized Bell function#✓fully proved

For complex numbers \(a\), \(b\), \(x\) and a natural number \(n\), the generalized Bell function is \(F(a, b, x; n) = e^{-x} \sum_{k=0}^{\infty} \frac{(a + b(k + 1))^n x^{k+1}}{k!}\).

noncomputable def generalizedBellGenerating (a b x : ℂ) (n : ℕ) : ℂ :=
  Complex.exp (-x) * ∑' (k : ℕ),
      ((a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (9.1).

Used by 10

Used byEntry 3 coefficients as generalized Bell values · Asymptotic expansion of Ramanujan's factorial series, for every \(x\) · Asymptotic expansion of Ramanujan's product series · Generalized Bell function extended to \(n = -1\) · Exponential generating function of Ramanujan's Bell-type series (Entry 4) · Binomial recurrence for Ramanujan's Bell-type series (Entry 5) · Exponential generating function of the generalized Bell function (Entry 9(ii)) · Convergence of the generalized Bell series · Ramanujan's integral formula with Bernoulli numbers · Integrability of the scaled generalized Bell integrand on \((0, 1)\)

TheoremConvergence of the generalized Bell series#✓fully proved

Let \(F\) denote Ramanujan's generalized Bell function. For complex numbers \(a\), \(b\), \(x\) and every natural number \(n\), the series \(\sum_{k=0}^{\infty} (a + b(k + 1))^n x^{k+1} / k!\) converges absolutely and its sum is \(e^{x} F(a, b, x; n)\).

theorem ramanujan_part1_ch3_entry9_ii_generalizedbellgenerating_defining (a b x : ℂ)
    (n : ℕ) :
    HasSum (fun k : ℕ => (a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))
      (Complex.exp x * generalizedBellGenerating a b x n)

noncomputable def generalizedBellGenerating (a b x : ℂ) (n : ℕ) : ℂ :=
  Complex.exp (-x) * ∑' (k : ℕ),
      ((a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry9IiGeneralizedbellgeneratingDefining.lean:31

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (9.1) printed p. 53/PDF p. 63 and Entry 9(ii), formula (9.4), printed p. 54/PDF p. 64.

Uses 1 · Used by 2

Statement usesRamanujan's generalized Bell function

Used byAsymptotic expansion of Ramanujan's product series · Binomial recurrence for Ramanujan's Bell-type series (Entry 5)

TheoremExponential generating function of Ramanujan's Bell-type series (Entry 4)#✓fully proved

Let \(F\) be Ramanujan's generalized Bell function. For all complex numbers \(a\) and \(x\), let \(f(x, n) = F(0, 1, x; n) = e^{-x} \sum_{j=0}^{\infty} \frac{(j+1)^n x^{j+1}}{j!}\) for natural numbers \(n\), and set \(f(x, -1) = 1\). Then the series \(\sum_{n=0}^{\infty} \frac{a^n}{n!} f(x, n-1)\) converges absolutely and its sum is \(e^{x(e^a - 1)}\).

theorem ramanujan_part1_ch3_entry4 (a x : ℂ) :
    HasSum (fun n : ℕ => a ^ n / (Nat.factorial n : ℂ) *
        (if n = 0 then (1 : ℂ) else generalizedBellGenerating 0 1 x (n - 1)))
        (Complex.exp (x * (Complex.exp a - 1))) ∧
      Summable (fun n : ℕ => ‖a ^ n / (Nat.factorial n : ℂ) *
          (if n = 0 then (1 : ℂ) else generalizedBellGenerating 0 1 x (n - 1))‖)

noncomputable def generalizedBellGenerating (a b x : ℂ) (n : ℕ) : ℂ :=
  Complex.exp (-x) * ∑' (k : ℕ),
      ((a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry9IiGeneralizedbellgeneratingDefining.lean:31

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 4, formula (4.1), printed pp. 47--48 / PDF pp. 57--58. The source's f(x, n) = e^{-x} ∑_{j ≥ 0} (j + 1)ⁿ xʲ⁺¹ / j! is generalizedBellGenerating 0 1 x n.

Uses 2

Statement usesRamanujan's generalized Bell function

Proof usesAbsolute convergence of Ramanujan's Bell-type series (Entry 4)

TheoremBinomial recurrence for Ramanujan's Bell-type series (Entry 5)#✓fully proved

Let \(F\) be Ramanujan's generalized Bell function. For every natural number \(n\) and every complex number \(x\), write \(f(x, m) = F(0, 1, x; m)\) for natural numbers \(m\), and set \(f(x, -1) = 1\). Then \(f(x, n) = x \sum_{k=0}^{n} \binom{n}{k} f(x, k-1)\).

theorem ramanujan_part1_ch3_entry5 (n : ℕ) (x : ℂ) :
    generalizedBellGenerating 0 1 x n = x *
        (Finset.range (n + 1)).sum (fun k => (Nat.choose n k : ℂ) *
            (if k = 0 then 1 else generalizedBellGenerating 0 1 x (k - 1)))

noncomputable def generalizedBellGenerating (a b x : ℂ) (n : ℕ) : ℂ :=
  Complex.exp (-x) * ∑' (k : ℕ),
      ((a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry9IiGeneralizedbellgeneratingDefining.lean:31

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 5, printed p. 48 / PDF p. 58.

Uses 2

Statement usesRamanujan's generalized Bell function

Proof usesConvergence of the generalized Bell series

TheoremExponential generating function of the generalized Bell function (Entry 9(ii))#✓fully proved

Let \(F(a, b, x; n)\) be Ramanujan's generalized Bell function. For all complex numbers \(a\), \(b\), \(x\) and \(y\), the series \(\sum_{n=0}^{\infty} \frac{y^n}{n!} F(a, b, x; n)\) converges to \(x e^{(a+b)y} e^{x(e^{by} - 1)}\).

theorem ramanujan_part1_ch3_entry9_ii_generalizedbellgenerating (a b x y : ℂ) :
    HasSum (fun n : ℕ => y ^ n / (Nat.factorial n : ℂ) * generalizedBellGenerating a b x n)
        (x * Complex.exp ((a + b) * y) * Complex.exp (x * (Complex.exp (b * y) - 1)))

noncomputable def generalizedBellGenerating (a b x : ℂ) (n : ℕ) : ℂ :=
  Complex.exp (-x) * ∑' (k : ℕ),
      ((a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry9IiGeneralizedbellgeneratingDefining.lean:31

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (9.1) printed p. 53/PDF p. 63 and Entry 9(ii), formula (9.4), printed p. 54/PDF p. 64. The source's F(a, b, x; n) is generalizedBellGenerating a b x n.

Uses 1

Statement usesRamanujan's generalized Bell function

DefinitionGeneralized Bell function extended to \(n = -1\)#✓fully proved

For an integer \(n \ge -1\) and a complex number \(x\), \(f(n, x) = 1\) if \(n = -1\), and otherwise \(f(n, x)\) is the generalized Bell function \(F(0, 1, x; n) = e^{-x} \sum_{k \ge 0} (k + 1)^n x^{k + 1} / k!\).

noncomputable def f (n : { n : ℤ // -1 ≤ n }) (x : ℂ) : ℂ :=
  if n.val = -1 then 1 else generalizedBellGenerating 0 1 x n.val.toNat

noncomputable def generalizedBellGenerating (a b x : ℂ) (n : ℕ) : ℂ :=
  Complex.exp (-x) * ∑' (k : ℕ),
      ((a + b * (↑(k + 1) : ℂ)) ^ n * x ^ (k + 1) / (↑(Nat.factorial k) : ℂ))

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry9IiGeneralizedbellgeneratingDefining.lean:31

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Section 8, Example 4 and its correction, printed pp. 51--52 / PDF pp. 61--62.

Uses 1 · Used by 2

Statement usesRamanujan's generalized Bell function

Used byRamanujan's integral formula with Bernoulli numbers · Integrability of the scaled generalized Bell integrand on \((0, 1)\)

TheoremIntegrability of the scaled generalized Bell integrand on \((0, 1)\)#✓fully proved

Let \(f\) be the generalized Bell function extended to \(n = -1\). For every natural number \(m\) and every complex number \(x\), the complex-valued function \(t \mapsto x f(m - 1, t x)\) of a real variable \(t\) is interval integrable on \([0, 1]\) with respect to Lebesgue measure.

theorem ramanujan_part1_ch3_section8_example4_integrable (m : ℕ) (x : ℂ) :
    IntervalIntegrable (fun t : ℝ => x * f ⟨(m : ℤ) - 1,
        by omega⟩ ((t : ℂ) * x)) MeasureTheory.volume 0 1

noncomputable def f (n : { n : ℤ // -1 ≤ n }) (x : ℂ) : ℂ :=
  if n.val = -1 then 1 else generalizedBellGenerating 0 1 x n.val.toNat

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Section8Example4Integrable.lean:34

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Section 8, Example 4 and its correction, printed pp. 51--52 / PDF pp. 61--62.

Uses 2

Statement usesGeneralized Bell function extended to \(n = -1\)

Proof usesRamanujan's generalized Bell function

TheoremRamanujan's integral formula with Bernoulli numbers#✓fully proved

Let \(f(-1, x) = 1\) and, for natural numbers \(n\), let \(f(n, x) = e^{-x} \sum_{j=0}^{\infty} (j + 1)^n x^{j+1} / j!\) for complex \(x\). Let \(B_n\) be the Bernoulli numbers, with \(B_1 = -1/2\). Then for every natural number \(m\) and every complex number \(x\),

\[\int_0^1 x\, f(m - 1, t x)\, dt = \sum_{k=0}^{m} \binom{m}{k} B_{m-k} \frac{f(k, x)}{k + 1}.\]

theorem ramanujan_part1_ch3_section8_example4_bernoulli_integral (m : ℕ) (x : ℂ) :
    ∫ (t : ℝ) in (0 : ℝ)..(1 : ℝ), x * f ⟨(↑m : ℤ) - 1, by omega⟩ ((↑t : ℂ) * x) =
      ∑ k ∈ Finset.range (m + 1), (↑(Nat.choose m k) : ℂ) * (↑(bernoulli (m - k)) : ℂ) *
          f ⟨↑k, by omega⟩ x / (↑(k + 1) : ℂ)

noncomputable def f (n : { n : ℤ // -1 ≤ n }) (x : ℂ) : ℂ :=
  if n.val = -1 then 1 else generalizedBellGenerating 0 1 x n.val.toNat

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Section8Example4Integrable.lean:34

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Section 8, Example 4 and its correction, printed pp. 51--52 / PDF pp. 61--62.

Uses 2

Statement usesGeneralized Bell function extended to \(n = -1\)

Proof usesRamanujan's generalized Bell function

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.