Asymptotic expansions of factorial series

DefinitionTerms of Ramanujan's factorial series#✓fully proved

For a real number \(x\) and a natural number \(j\), the \(j\)-th term of Ramanujan's factorial series is \((-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\), read as \(0\) when the denominator vanishes.

def chapter6Section13ExampleCTerm (x : ℝ) (j : ℕ) : ℝ :=
  (-1 : ℝ) ^ j /
    ∏ r ∈ range (j + 1), (x + (r + 1 : ℕ))
Used by 6
Used byRamanujan's factorial series · Functional equation of Ramanujan's factorial series · Recursion for the terms of Ramanujan's factorial series · Asymptotic expansion of Ramanujan's factorial series · Convergence and asymptotic expansion of Ramanujan's factorial series · Convergence of Ramanujan's factorial series

DefinitionRamanujan's factorial series#✓fully proved

For a real number \(x\), \(C(x)\) is the sum \(\sum_{j \ge 0} (-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\) of Ramanujan's factorial series, where a term is read as \(0\) when its denominator vanishes and the sum is taken to be \(0\) when the series is not summable.

The series is summable for every \(x > 0\).

def chapter6Section13ExampleCSum (x : ℝ) : ℝ :=
  ∑' j : ℕ, chapter6Section13ExampleCTerm x j
Uses 1 · Used by 3
Statement usesTerms of Ramanujan's factorial series
Used byFunctional equation of Ramanujan's factorial series · Asymptotic expansion of Ramanujan's factorial series · Convergence and asymptotic expansion of Ramanujan's factorial series

TheoremConvergence of Ramanujan's factorial series#✓fully proved

For every real \(x > 0\), the series \(\sum_{j \ge 0} (-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\) is summable.

Its \(j\)-th term is bounded in absolute value by \(1 / (j + 1)!\).

theorem summable_chapter6Section13ExampleCTerm (x : ℝ) (hx : 0 < x) :
    Summable (chapter6Section13ExampleCTerm x)
Uses 1 · Used by 2
Statement usesTerms of Ramanujan's factorial series
Used byFunctional equation of Ramanujan's factorial series · Convergence and asymptotic expansion of Ramanujan's factorial series

TheoremRecursion for the terms of Ramanujan's factorial series#✓fully proved

Write \(c_j(x) = (-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\) for the \(j\)-th term of Ramanujan's factorial series, with division by \(0\) read as \(0\). For every real \(x\) and every natural number \(j\), \(c_{j+1}(x) = -\frac{1}{x + 1} \, c_j(x + 1)\).

theorem chapter6Section13ExampleCTerm_succ (x : ℝ) (j : ℕ) :
    chapter6Section13ExampleCTerm x (j + 1) =
      (-1 / (x + 1)) * chapter6Section13ExampleCTerm (x + 1) j
Uses 1 · Used by 1
Statement usesTerms of Ramanujan's factorial series
Used byFunctional equation of Ramanujan's factorial series

TheoremFunctional equation of Ramanujan's factorial series#✓fully proved

Let \(C(x) = \sum_{j \ge 0} (-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\) be Ramanujan's factorial series. For every real \(x > 0\), \(C(x) = \frac{1}{x + 1} - \frac{C(x + 1)}{x + 1}\).

theorem chapter6Section13ExampleCSum_eq (x : ℝ) (hx : 0 < x) :
    chapter6Section13ExampleCSum x =
      1 / (x + 1) - chapter6Section13ExampleCSum (x + 1) / (x + 1)
Uses 4 · Used by 1
Statement usesRamanujan's factorial series
Proof usesTerms of Ramanujan's factorial series · Recursion for the terms of Ramanujan's factorial series · Convergence of Ramanujan's factorial series
Used byAsymptotic expansion of Ramanujan's factorial series

TheoremAsymptotic expansion of Ramanujan's factorial series#✓fully proved

Let \(C(x) = \sum_{j \ge 0} (-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\) be Ramanujan's factorial series and let \(B_n\) denote the \(n\)-th Bell number. For every natural number \(N\),

\[C(x) - \sum_{j=0}^{N-1} \frac{(-1)^j B_{j+1}}{x^{j+1}} = O\left(\frac{1}{x^{N+1}}\right) \quad \text{as } x \to \infty.\]
theorem isBigO_chapter6Section13ExampleCSum_sub_sum_bell (N : ℕ) :
    (fun x : ℝ => chapter6Section13ExampleCSum x -
        ∑ j ∈ range N, (-1 : ℝ) ^ j * ((j + 1).bell : ℝ) / x ^ (j + 1))
      =O[atTop] (fun x : ℝ => 1 / x ^ (N + 1))
Uses 3 · Used by 1
Statement usesRamanujan's factorial series
Proof usesFunctional equation of Ramanujan's factorial series · Terms of Ramanujan's factorial series
Used byConvergence and asymptotic expansion of Ramanujan's factorial series

TheoremConvergence and asymptotic expansion of Ramanujan's factorial series#✓fully proved

Let \(c_j(x) = (-1)^j / ((x + 1)(x + 2) \cdots (x + j + 1))\), let \(C(x) = \sum_{j \ge 0} c_j(x)\), and let \(B_n\) denote the \(n\)-th Bell number. For all sufficiently large real \(x\), \(x > 0\) and the series \(\sum_{j \ge 0} c_j(x)\) is summable; and for every natural number \(N\),

\[C(x) - \sum_{j=0}^{N-1} \frac{(-1)^j B_{j+1}}{x^{j+1}} = O\left(\frac{1}{x^{N+1}}\right) \quad \text{as } x \to \infty.\]
theorem ramanujan_part1_ch6_entry5_digamma :
    (∀ᶠ x : ℝ in atTop,
        0 < x ∧ Summable (chapter6Section13ExampleCTerm x)) ∧
      ∀ N : ℕ, Asymptotics.IsBigO atTop
        (fun x : ℝ => chapter6Section13ExampleCSum x -
          ∑ j ∈ range N,
            (-1 : ℝ) ^ j * ((j + 1).bell : ℝ) /
              x ^ (j + 1))
        (fun x : ℝ => 1 / x ^ (N + 1))
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 6.
Uses 4
Statement usesRamanujan's factorial series · Terms of Ramanujan's factorial series
Proof usesAsymptotic expansion of Ramanujan's factorial series · Convergence of Ramanujan's factorial series

TheoremSummability of Ramanujan's factorial series in a sector, for every \(x\)#✓fully proved

Let \(x\) be a complex number and let \(\varepsilon > 0\) be a real number. Then there is a real number \(R\) such that for every complex number \(z\) with \(|z| \ge R\) whose principal argument satisfies \(-\pi + \varepsilon \le \arg z \le \pi - \varepsilon\), the series \(\sum_{j=0}^{\infty} \frac{(-1)^j x^{j+1}}{(z+1)(z+2)\cdots(z+j+1)}\) is summable.

theorem ramanujan_part1_ch3_entry3_psisummable_general (x : ℂ) (ε : ℝ) (hε₁ : 0 < ε) :
    ∃ R : ℝ, ∀ z : ℂ, R ≤ ‖z‖ → -Real.pi + ε ≤ Complex.arg z → Complex.arg z ≤ Real.pi - ε →
      Summable (fun j : ℕ => (-1 : ℂ) ^ j * x ^ (j + 1) / ∏ k ∈ Finset.range (j + 1),
          (z + (↑(k + 1) : ℂ)))
Uses 1 · Used by 1
Proof usesSummability of a rising-product series
Used bySummability of Ramanujan's factorial series in a sector

TheoremSummability of Ramanujan's factorial series in a sector#✓fully proved

Let \(x\) be a nonzero complex number and let \(\varepsilon\) be a real number with \(0 < \varepsilon < \pi\). Then there is a real number \(R\) such that for every complex number \(z\) with \(|z| \ge R\) whose principal argument satisfies \(-\pi + \varepsilon \le \arg z \le \pi - \varepsilon\), the series \(\sum_{j=0}^{\infty} \frac{(-1)^j x^{j+1}}{(z+1)(z+2)\cdots(z+j+1)}\) is summable.

The hypotheses \(x \neq 0\) and \(\varepsilon < \pi\) are not needed for the proof; they are kept to match the source.

@[nolint unusedArguments]
theorem ramanujan_part1_ch3_entry3_psisummable (x : ℂ)
    (hx : x ≠ 0) (ε : ℝ) (hε₁ : 0 < ε) (hε₂ : ε < Real.pi) :
    ∃ R : ℝ, ∀ z : ℂ, R ≤ ‖z‖ → -Real.pi + ε ≤ Complex.arg z → Complex.arg z ≤ Real.pi - ε →
      Summable (fun j : ℕ => (-1 : ℂ) ^ j * x ^ (j + 1) / ∏ k ∈ Finset.range (j + 1),
          (z + (↑(k + 1) : ℂ)))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 3, printed p. 47 / PDF p. 57. It follows from ramanujan_part1_ch3_entry3_psisummable_general; the hypotheses x ≠ 0 and ε < π are unused and keep the source's shape.
Uses 1
Proof usesSummability of Ramanujan's factorial series in a sector, for every \(x\)

DefinitionRamanujan's product series#✓fully proved

For complex numbers \(a\), \(b\), \(x\), \(z\), Ramanujan's product series of Entry 9(i) is

\[P(a, b, x; z) = \sum_{j=0}^{\infty} \frac{(-b)^j x^{j+1}}{\prod_{r=0}^{j} (z + a + b(r + 1))}.\]

The definition is totalized: a quotient with vanishing denominator is taken to be \(0\), and the sum of a non-summable series is taken to be \(0\). Hence at a pole of the source expression, for example \(a = 0\), \(b = 1\), \(x = 1\), \(z = -1\), where every product contains the vanishing factor \(z + a + b = 0\), every term and so \(P\) itself equals \(0\), whereas the source expression has a singularity there. Off the poles, when \(b \neq 0\) and \(w = (z + a)/b\) is nonzero and satisfies \(|\arg w| \le \pi - \varepsilon\) for some \(0 < \varepsilon < \pi\), the closed form of Ramanujan's product series identifies \(P\) with the source's closed form.

noncomputable def entry9_P (a b x : ℂ) (z : ℂ) : ℂ :=
  ∑' (j : ℕ), ((-b) ^ j * x ^ (j + 1) / ∏ r ∈ Finset.range (j + 1), (z + a + b * ((r : ℂ) + 1)))
Used by 4
Used byClosed form of Ramanujan's product series off the poles · Ramanujan's factorial series as the Entry 9 product series at \(a = 0\), \(b = 1\) · Asymptotic expansion of Ramanujan's factorial series, for every \(x\) · Asymptotic expansion of Ramanujan's product series

TheoremClosed form of Ramanujan's product series off the poles#✓fully proved

Let \(a, b, x, z \in \mathbb{C}\) with \(b \neq 0\), let \(0 < \varepsilon < \pi\), and put \(w = (z + a)/b\). Suppose that \(w \neq 0\), that \(-\pi + \varepsilon \le \arg w \le \pi - \varepsilon\), and that \(w + r + 1 \neq 0\) for every natural number \(r\). Then Ramanujan's product series \(P\) satisfies

\[P(a, b, x; z) = e^{-x} \sum_{m=0}^{\infty} \frac{x^{m+1}}{m!\,(z + a + b(m + 1))}.\]
theorem entry9_P_closed (a b x z w : ℂ) (ε : ℝ)
    (hεpos : 0 < ε) (hεlt : ε < Real.pi)
    (hb : b ≠ 0)
    (h1 : -Real.pi + ε ≤ Complex.arg w) (h2 : Complex.arg w ≤ Real.pi - ε)
    (hwpos : 0 < ‖w‖) (hz : (z + a) / b = w)
    (hw : ∀ r : ℕ, w + ((r : ℂ) + 1) ≠ 0) :
    entry9_P a b x z = Complex.exp (-x) * ∑' (m : ℕ),
      (x ^ (m + 1) / ((Nat.factorial m : ℂ) * (z + (a + b * ((m : ℂ) + 1)))))
Uses 1 · Used by 1
Statement usesRamanujan's product series
Used byAsymptotic expansion of Ramanujan's product series

TheoremAsymptotic expansion of Ramanujan's product series#✓fully proved

Let \(a, b, x \in \mathbb{C}\) with \(b \neq 0\), let \(0 < \varepsilon < \pi\), and let \(n\) be a natural number. Write \(F(a, b, x; k)\) for Ramanujan's generalized Bell function and \(P(a, b, x; z)\) for Ramanujan's product series. Then

\[P(a, b, x; z) = \sum_{k=0}^{n} \frac{(-1)^k F(a, b, x; k)}{z^{k+1}} + O(|z|^{-n-2})\]

as \(|(z + a)/b| \to \infty\) with \(-\pi + \varepsilon \le \arg((z + a)/b) \le \pi - \varepsilon\): there are real numbers \(C\) and \(R\) such that the difference of the two sides has absolute value at most \(C / |z|^{n+2}\) for every complex \(z\) with \(|(z + a)/b| \ge R\) and \(-\pi + \varepsilon \le \arg((z + a)/b) \le \pi - \varepsilon\).

theorem ramanujan_part1_ch3_entry9_odd (a b x : ℂ)
    (hb : b ≠ 0) (ε : ℝ) (hεpos : 0 < ε) (hεlt : ε < Real.pi) (n : ℕ) :
    Asymptotics.IsBigO
      (Filter.comap (fun z : ℂ => (z + a) / b)
        (Filter.cocompact ℂ ⊓ Filter.principal {w : ℂ | -Real.pi + ε ≤ Complex.arg w ∧
            Complex.arg w ≤ Real.pi - ε}))
      (fun z : ℂ =>
          (Finset.sum (Finset.range (n + 1))
              (fun k => ((-1 : ℂ) ^ k * generalizedBellGenerating a b x k) / z ^ (k + 1)) -
            entry9_P a b x z))
      (fun z : ℂ => (1 : ℂ) / z ^ (n + 2))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 9(i), definitions printed p. 53 / PDF p. 63 and result printed p. 54 / PDF p. 64.
Uses 4 · Used by 1
Statement usesRamanujan's generalized Bell function · Ramanujan's product series
Proof usesConvergence of the generalized Bell series · Closed form of Ramanujan's product series off the poles
Used byAsymptotic expansion of Ramanujan's factorial series, for every \(x\)

TheoremEntry 3 coefficients as generalized Bell values#✓fully proved

Let \(F\) be Ramanujan's generalized Bell function. For every complex number \(x\) and every natural number \(j\), let \(f(x, j) = e^{-x} \sum_{k=0}^{\infty} \frac{(k+1)^j x^{k+1}}{k!}\). Then \(f(x, j) = F(0, 1, x; j)\).

theorem fCoeff_eq_generalizedBellGenerating (x : ℂ) (j : ℕ) :
    fCoeff x j =
      Entry9IiGeneralizedbellgeneratingDefining.generalizedBellGenerating 0 1 x j
Uses 1 · Used by 1
Statement usesRamanujan's generalized Bell function
Used byAsymptotic expansion of Ramanujan's factorial series, for every \(x\)

TheoremRamanujan's factorial series as the Entry 9 product series at \(a = 0\), \(b = 1\)#✓fully proved

Let \(P\) be Ramanujan's Entry 9(i) product series. For all complex numbers \(x\) and \(z\), let \(\psi(x, z) = \sum_{j=0}^{\infty} t_j\), where \(t_j = \frac{(-1)^j x^{j+1}}{(z+1)(z+2)\cdots(z+j+1)}\) when the product in the denominator is nonzero and \(t_j = 0\) otherwise. Then \(\psi(x, z) = P(0, 1, x; z)\).

Since division by zero is taken to give zero, the case distinction in \(t_j\) changes nothing.

theorem psi_eq_entry9_P (x z : ℂ) :
    psi x z = Entry9Odd.entry9_P 0 1 x z
Uses 1 · Used by 1
Statement usesRamanujan's product series
Used byAsymptotic expansion of Ramanujan's factorial series, for every \(x\)

TheoremAsymptotic expansion of Ramanujan's factorial series, for every \(x\)#✓fully proved

Let \(x\) be a complex number. For natural numbers \(j\) let \(f(x, j) = e^{-x} \sum_{k=0}^{\infty} \frac{(k+1)^j x^{k+1}}{k!}\), and for complex \(z\) let \(\psi(x, z) = \sum_{j=0}^{\infty} t_j\), where \(t_j = \frac{(-1)^j x^{j+1}}{(z+1)(z+2)\cdots(z+j+1)}\) when the denominator is nonzero and \(t_j = 0\) otherwise. Let \(\varepsilon\) be a real number with \(0 < \varepsilon < \pi\), and let \(S_\varepsilon\) be the set of complex \(z\) whose principal argument satisfies \(-\pi + \varepsilon \le \arg z \le \pi - \varepsilon\). Then for every natural number \(N\),

\[\psi(x, z) - \sum_{j=0}^{N} \frac{(-1)^j f(x, j)}{z^{j+1}} = O\left(\frac{1}{z^{N+2}}\right)\]

as \(|z| \to \infty\) with \(z \in S_\varepsilon\).

theorem ramanujan_part1_ch3_entry3_general (x : ℂ)
    (ε : ℝ) (hε_pos : 0 < ε) (hε_lt : ε < Real.pi) (N : ℕ) :
    Asymptotics.IsBigO (Filter.cocompact ℂ ⊓ Filter.principal (sector ε))
      (fun z : ℂ => psi x z - ∑ j ∈ Finset.range (N + 1), ((-1 : ℂ) ^ j * fCoeff x j / z ^ (j + 1)))
      (fun z : ℂ => (1 : ℂ) / z ^ (N + 2))
Uses 5 · Used by 1
Proof usesEntry 3 coefficients as generalized Bell values · Ramanujan's factorial series as the Entry 9 product series at \(a = 0\), \(b = 1\) · Ramanujan's generalized Bell function · Ramanujan's product series · Asymptotic expansion of Ramanujan's product series
Used byRamanujan's asymptotic expansion of a factorial series

TheoremRamanujan's asymptotic expansion of a factorial series#✓fully proved

Let \(x\) be a nonzero complex number. For natural numbers \(j\) let \(f(x, j) = e^{-x} \sum_{k=0}^{\infty} \frac{(k+1)^j x^{k+1}}{k!}\), and for complex \(z\) let \(\psi(x, z) = \sum_{j=0}^{\infty} t_j\), where \(t_j = \frac{(-1)^j x^{j+1}}{(z+1)(z+2)\cdots(z+j+1)}\) when the denominator is nonzero and \(t_j = 0\) otherwise. Let \(\varepsilon\) be a real number with \(0 < \varepsilon < \pi\), and let \(S_\varepsilon\) be the set of complex \(z\) whose principal argument satisfies \(-\pi + \varepsilon \le \arg z \le \pi - \varepsilon\). Then for every natural number \(N\),

\[\psi(x, z) - \sum_{j=0}^{N} \frac{(-1)^j f(x, j)}{z^{j+1}} = O\left(\frac{1}{z^{N+2}}\right)\]

as \(|z| \to \infty\) with \(z \in S_\varepsilon\).

The hypothesis \(x \neq 0\) is not needed for the proof; it is kept to match the source.

theorem ramanujan_part1_ch3_entry3 (x : ℂ)
    (hx : x ≠ 0) (ε : ℝ) (hε_pos : 0 < ε) (hε_lt : ε < Real.pi) (N : ℕ) :
    Asymptotics.IsBigO (Filter.cocompact ℂ ⊓ Filter.principal (sector ε))
      (fun z : ℂ => psi x z - ∑ j ∈ Finset.range (N + 1), ((-1 : ℂ) ^ j * fCoeff x j / z ^ (j + 1)))
      (fun z : ℂ => (1 : ℂ) / z ^ (N + 2))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 3, printed p. 47 / PDF p. 57.
Uses 1
Proof usesAsymptotic expansion of Ramanujan's factorial series, for every \(x\)

TheoremConvergence of Ramanujan's product series in a sector#✓fully proved

Let \(a, b, x \in \mathbb{C}\) with \(b \neq 0\) and let \(0 < \varepsilon < \pi\). Then there is a real number \(R\) such that for every complex \(z\) with \(|(z + a)/b| \ge R\) and \(-\pi + \varepsilon \le \arg((z + a)/b) \le \pi - \varepsilon\), the series

\[\sum_{j=0}^{\infty} \frac{(-b)^j x^{j+1}}{\prod_{r=0}^{j} (z + a + b(r + 1))}\]

converges absolutely.

theorem ramanujan_part1_ch3_entry9_odd_productsummable (a b x : ℂ)
    (hb : b ≠ 0) (ε : ℝ) (hεpos : 0 < ε) (hεlt : ε < Real.pi) :
    ∃ R : ℝ, ∀ z : ℂ, R ≤ ‖(z + a) / b‖ → -Real.pi + ε ≤ Complex.arg ((z + a) / b) →
        Complex.arg ((z + a) / b) ≤ Real.pi - ε →
            Summable (fun j : ℕ =>
                ((-b) ^ j * x ^ (j + 1) / ∏ r ∈ Finset.range (j + 1),
                    (z + a + b * ((r + 1 : ℕ) : ℂ))))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 9(i), definitions printed p. 53 / PDF p. 63 and result printed p. 54 / PDF p. 64. It follows from Complex.summable_neg_pow_mul_pow_div_prod_add_mul: the upper sector bound keeps (z + a) / b off the negative real axis, so no factor of the denominator vanishes. The hypothesis hεlt, the radius (taken to be 0) and the lower sector bound are unused and keep the source's shape.
Uses 1
Proof usesSummability of a rising-product series

TheoremAsymptotic expansion of a factorial series#✓fully proved

Let \(a_0, a_1, \ldots\) be complex numbers, let \(\psi : \mathbb{C} \to \mathbb{C}\), let \(\lambda\) be either a real number or \(-\infty\), and let \(0 < \varepsilon < \pi/2\). Suppose that for every complex \(z\) that is not a negative integer and satisfies \(\operatorname{Re} z > \lambda\), the series

\[\sum_{j=0}^{\infty} \frac{(-1)^j a_j}{(z + 1)(z + 2) \cdots (z + j + 1)}\]

converges absolutely with sum \(\psi(z)\). Write \(S(n, k)\) for the Stirling numbers of the second kind and \(c_j = \sum_{k=0}^{j} a_k S(j + 1, k + 1)\). Then for every natural number \(N\) there are real numbers \(C \ge 0\) and \(R > 0\) such that

\[\Big|\psi(z) - \sum_{j=0}^{N} \frac{(-1)^j c_j}{z^{j+1}}\Big| \le \frac{C}{|z|^{N+2}}\]

for every complex \(z\) that is not a negative integer, satisfies \(\operatorname{Re} z > \lambda\) and \(|z| \ge R\), and lies in the sector \(|\arg z| \le \pi/2 - \varepsilon\) when \(\lambda = -\infty\), or \(|\arg(z - \lambda)| \le \pi/2 - \varepsilon\) when \(\lambda\) is real.

For \(\lambda = -\infty\) the expansion is stated on the sector \(|\arg z| \le \pi/2 - \varepsilon\), as for real \(\lambda\); on the wider sector \(|\arg z| \le \pi - \varepsilon\) it fails, for example for \(a_j = j!\,(-2/3)^j\).

Proof: Use convergence at one real point to obtain absolute convergence two units to the right, then expand each \(1/((z + 1)\cdots(z + j + 1))\) termwise in powers of \(1/z\) and bound the tail.

MathlibExt.NumberTheory.Ramanujan.Part1Ch3.Section8Example1Asymptotic.ramanujan_part1_ch3_section8_example1_asymptotic · 21 lines 
theorem ramanujan_part1_ch3_section8_example1_asymptotic
  (a : ℕ → ℂ)
  (ψ : ℂ → ℂ)
  (lam : WithBot ℝ)
  (eps : ℝ)
  (heps_pos : 0 < eps)
  (heps_lt_pi_div_two : lam ≠ (⊥ : WithBot ℝ) → eps < Real.pi / 2)
  (heps_lt_pi_div_two_bot : lam = (⊥ : WithBot ℝ) → eps < Real.pi / 2)
  (hsum : ∀ z : ℂ, (∀ n : ℕ, z ≠ -((n + 1 : ℕ) : ℂ)) → lam < (↑z.re : WithBot ℝ) →
      HasSum (fun j : ℕ => (-1 : ℂ) ^ j * a j / ∏ k ∈ Finset.range (j + 1), (z + ((k + 1 : ℕ) : ℂ)))
          (ψ z)) :
    ∀ N : ℕ, ∃ C : ℝ, ∃ R : ℝ, 0 < R ∧ 0 ≤ C ∧ ∀ z : ℂ, (∀ n : ℕ, z ≠ -((n + 1 : ℕ) : ℂ)) →
        lam < (↑z.re : WithBot ℝ) →
            ((lam = (⊥ : WithBot ℝ) → |Complex.arg z| ≤ Real.pi / 2 - eps) ∧
                (∀ r : ℝ, lam = (↑r : WithBot ℝ) → |Complex.arg (z - (r : ℂ))| ≤ Real.pi /
                    2 - eps)) →
                R ≤ ‖z‖ → ‖ψ z - ∑ j ∈ Finset.range (N + 1),
                    ((-1 : ℂ) ^ j *
                        (∑ k ∈ Finset.range (j + 1), a k *
                            ((Nat.stirlingSecond (j + 1) (k + 1) : ℕ) : ℂ)) / z ^ (j + 1))‖ ≤ C /
                            ‖z‖ ^ (N + 2)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Section 8, Example 1, formula (8.1), printed p. 50 / PDF p. 60.

TheoremConvergence of a factorial series in a sector, general form#✓fully proved

Let \(a_0, a_1, \ldots\) be complex numbers, let \(\lambda\) be either a real number or \(-\infty\), and let \(\varepsilon > 0\). Suppose that the series

\[\sum_{j=0}^{\infty} \frac{(-1)^j a_j}{(z + 1)(z + 2) \cdots (z + j + 1)}\]

converges absolutely for every complex \(z\) that is not a negative integer and satisfies \(\operatorname{Re} z > \lambda\). Then there is a real number \(R\) such that the series converges absolutely for every complex \(z\) with \(|z| > R\) that lies in the sector \(|\arg(z - \lambda)| \le \pi/2 - \varepsilon\) when \(\lambda\) is real, or \(|\arg z| \le \pi - \varepsilon\) when \(\lambda = -\infty\).

theorem ramanujan_part1_ch3_section8_example1_summable_general
    (a : ℕ → ℂ) (lam : Option ℝ) (eps : ℝ) (heps_pos : 0 < eps)
    (hSumm : ∀ z : ℂ, (∀ n : ℕ, z ≠ -((n + 1 : ℕ) : ℂ)) →
      (∀ l : ℝ, lam = some l → l < z.re) →
      Summable (fun j : ℕ => ((-1 : ℂ) ^ j * a j) /
        ((Finset.range (j + 1)).prod fun k : ℕ => z + ((k + 1 : ℕ) : ℂ)))) :
    ∃ R : ℝ, ∀ z : ℂ, sector lam eps z → R < ‖z‖ →
        Summable (fun j : ℕ => ((-1 : ℂ) ^ j * a j) /
            ((Finset.range (j + 1)).prod fun k : ℕ => z + ((k + 1 : ℕ) : ℂ)))
Used by 1
Used byConvergence of a factorial series in a sector

TheoremConvergence of a factorial series in a sector#✓fully proved

Let \(a_0, a_1, \ldots\) be complex numbers, let \(\lambda\) be either a real number or \(-\infty\), and let \(\varepsilon > 0\), with \(\varepsilon < \pi/2\) when \(\lambda\) is real and \(\varepsilon < \pi\) when \(\lambda = -\infty\). Suppose that the series

\[\sum_{j=0}^{\infty} \frac{(-1)^j a_j}{(z + 1)(z + 2) \cdots (z + j + 1)}\]

converges absolutely for every complex \(z\) that is not a negative integer and satisfies \(\operatorname{Re} z > \lambda\). Then there is a real number \(R\) such that the series converges absolutely for every complex \(z\) with \(|z| > R\) that lies in the sector \(|\arg(z - \lambda)| \le \pi/2 - \varepsilon\) when \(\lambda\) is real, or \(|\arg z| \le \pi - \varepsilon\) when \(\lambda = -\infty\).

theorem ramanujan_part1_ch3_section8_example1_summable
    (a : ℕ → ℂ) (lam : Option ℝ) (eps : ℝ) (heps_pos : 0 < eps)
    (heps_lt : match lam with | some _ => eps < Real.pi / 2 | none => eps < Real.pi)
    (hSumm : ∀ z : ℂ, (∀ n : ℕ, z ≠ -((n + 1 : ℕ) : ℂ)) →
      (∀ l : ℝ, lam = some l → l < z.re) →
      Summable (fun j : ℕ => ((-1 : ℂ) ^ j * a j) /
        ((Finset.range (j + 1)).prod fun k : ℕ => z + ((k + 1 : ℕ) : ℂ)))) :
    ∃ R : ℝ, ∀ z : ℂ, sector lam eps z → R < ‖z‖ →
        Summable (fun j : ℕ => ((-1 : ℂ) ^ j * a j) /
            ((Finset.range (j + 1)).prod fun k : ℕ => z + ((k + 1 : ℕ) : ℂ)))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Section 8, Example 1, formula (8.1), printed p. 50 / PDF p. 60. It follows from ramanujan_part1_ch3_section8_example1_summable_general; the upper bound heps_lt is unused and keeps the source's shape.
Uses 1
Proof usesConvergence of a factorial series in a sector, general form
20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.