Abel-type exponential series

TheoremAbsolute convergence of the shifted series in Entry 12 for every \(n\)#✓fully proved

Let \(r\) be an integer and let \(n\) and \(a\) be complex numbers with \(|a| > e\), or with \(a = e\) and \(r \le -2\). Then

\[\sum_{k=0}^{\infty} \left| \frac{(n+k)^{r+1+k}}{a^k\, k!} \right| < \infty,\]

where integer powers of complex numbers follow the convention \(0^m = 0\) for \(m < 0\).

Unlike the version that assumes \(n + k \ne 0\) whenever \(k \ge 0\) and \(r + k < 0\), nothing is assumed about \(n\). At an index where \(n + k = 0\) and the exponent \(r + 1 + k\) is negative, the term is \(0^{r+1+k} = 0\), whereas the source's term is undefined there. Summability depends only on the tail, where every exponent is nonnegative.

theorem ramanujan_part1_ch3_entry12_summable_succ_n_general (r : ℤ) (n a : ℂ)
    (ha : norm a > Real.exp 1 ∨ (a = ↑(Real.exp 1) ∧ r ≤ -2)) :
    Summable (fun k : ℕ => norm ((n + (k : ℂ)) ^ (r + 1 + (k : ℤ)) / ((a ^ k) * (k.factorial : ℂ))))

Used by 4

Used byRamanujan's recurrence for the series in Entry 12 · Absolute convergence of the series in Entry 12 · Absolute convergence of the shifted series in Entry 12 · Ramanujan's \(\psi\)-series (Chapter 3, Entry 16)

TheoremAbsolute convergence of the shifted series in Entry 12#✓fully proved

Let \(r\) be an integer and let \(n\) and \(a\) be complex numbers. Suppose that \(|a| > e\), or that \(a = e\) and \(r \le -2\), and that \(n + k \ne 0\) for every integer \(k \ge 0\) with \(r + k < 0\). Then

\[\sum_{k=0}^{\infty} \left| \frac{(n+k)^{r+1+k}}{a^k\, k!} \right| < \infty.\]

theorem ramanujan_part1_ch3_entry12_summable_succ_n (r : ℤ) (n a : ℂ)
    (ha : norm a > Real.exp 1 ∨ (a = ↑(Real.exp 1) ∧ r ≤ -2))
    (hn : ∀ k : ℤ, 0 ≤ k → r + k < 0 → n + (k : ℂ) ≠ 0) :
    Summable (fun k : ℕ => norm ((n + (k : ℂ)) ^ (r + 1 + (k : ℤ)) / ((a ^ k) * (k.factorial : ℂ))))

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (12.1) and Entry 12, printed pp. 66-67 / PDF pp. 76-77.

Uses 1

Proof usesAbsolute convergence of the shifted series in Entry 12 for every \(n\)

TheoremRamanujan's recurrence for the series in Entry 12#✓fully proved

Fix a complex number \(a\). For an integer \(r\) and a complex number \(n\), let

\[F_r(n) = \sum_{k=0}^{\infty} \frac{(n+k)^{r+k}}{a^k\, k!},\]

where the sum is taken to be \(0\) if the series is not summable. Suppose that \(|a| > e\), or that \(a = e\) and \(r \le -2\), and that \(n + k \ne 0\) for every natural number \(k\) with \(r + k < 0\). Then

\[F_{r+1}(n) = n F_r(n) + \frac{1}{a} F_{r+1}(n+1).\]

theorem ramanujan_part1_ch3_entry12 (r : ℤ) (n a : ℂ)
    (ha : ‖a‖ > Real.exp 1 ∨ (a = (Real.exp 1 : ℂ) ∧ r ≤ -2))
    (hn : ∀ k : ℕ, r + (k : ℤ) < 0 → n + (k : ℂ) ≠ 0) :
    F (r + 1) n a = n * F r n a + (1 / a) * F (r + 1) (n + 1) a

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (12.1) and Entry 12, printed pp. 66-67 / PDF pp. 76-77.

Uses 1 · Used by 1

Proof usesAbsolute convergence of the shifted series in Entry 12 for every \(n\)

Used byRamanujan's three-term recurrence (Chapter 3, Entry 16(a))

TheoremAbsolute convergence of the series in Entry 12#✓fully proved

Let \(r\) be an integer and let \(n\) and \(a\) be complex numbers. Suppose that \(|a| > e\), or that \(a = e\) and \(r \le -2\), and that \(n + k \ne 0\) for every natural number \(k\) with \(r + k < 0\). Then

\[\sum_{k=0}^{\infty} \left| \frac{(n+k)^{r+k}}{a^k\, k!} \right| < \infty.\]

theorem ramanujan_part1_ch3_entry12_summable_r_n (r : ℤ)
    (n a : ℂ)
        (ha : ‖a‖ > Real.exp 1 ∨ (a = (Real.exp 1 : ℂ) ∧ r ≤ -2))
            (hn : ∀ k : ℕ, r + (k : ℤ) < 0 → n + (k : ℂ) ≠ 0) :
    Summable (fun k : ℕ => ‖(n + (k : ℂ)) ^ (r + (k : ℤ)) / (a ^ k * (Nat.factorial k : ℂ))‖)

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (12.1) and Entry 12, printed pp. 66-67 / PDF pp. 76-77.

Uses 1

Proof usesAbsolute convergence of the shifted series in Entry 12 for every \(n\)

TheoremRamanujan's three-term recurrence (Chapter 3, Entry 16(a))#✓fully proved

Let \(a\), \(x\), \(n\) be complex numbers and \(r\) an integer, where \(x \ne 0\) and \(x = a \log x\) with \(\log\) the principal branch of the complex logarithm. Suppose that \(|a| > e\), or that \(a = e\) and \(r \le -2\), and that \(n + k \ne 0\) for every natural number \(k\) with \(r + k < 0\). For an integer \(s\) and a complex number \(m\) put

\[\varphi(s, m) = e^{-m \log x} \sum_{k=0}^{\infty} \frac{(m + k)^{s + k}}{a^k\, k!};\]

the three series used below converge absolutely under these hypotheses. Then

\[n\, \varphi(r, n) = \varphi(r + 1, n) - \log x \cdot \varphi(r + 1, n + 1).\]

theorem ramanujan_part1_ch3_entry16 (a x n : ℂ)
    (r : ℤ)
        (hx_ne : x ≠ 0)
            (hx_eq : x = a * Complex.log x)
                (ha : ‖a‖ > Real.exp 1 ∨ (a = (Real.exp 1 : ℂ) ∧ r ≤ -2))
                    (hn : ∀ k : ℕ, r + (k : ℤ) < 0 → n + (k : ℂ) ≠ 0) :
    n * varphi a x r n = varphi a x (r + 1) n - Complex.log x * varphi a x (r + 1) (n + 1)

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, definition (12.1) printed p. 66 / PDF p. 76, Entry 12 p. 67 / PDF p. 77, and Entry 16(a) p. 78 / PDF p. 88. The series is Entry12.F, and the recurrence is Entry12.ramanujan_part1_ch3_entry12 multiplied by exp (-n * log x).

Uses 1

Proof usesRamanujan's recurrence for the series in Entry 12

TheoremJensen's series (Chapter 3, Entry 16, Corollary 1)#✓fully proved

Let \(\rho\) be a positive real number with \(\rho e^{\rho + 1} = 1\), let \(n\) be a real number with \(-\rho < n < 1\), and let \(x\) be a complex number. Then the series

\[\sum_{k=0}^{\infty} \frac{(x + kn)^k}{k!\, e^{kn}}\]

converges unconditionally to \(e^x / (1 - n)\).

theorem ramanujan_part1_ch3_entry16_corollary1_jensen_series (ρ : ℝ)
    (hρ_pos : 0 < ρ) (hρ_eq : ρ * Real.exp (ρ + 1) = 1) (n : ℝ) (hn : -ρ < n ∧ n < 1) (x : ℂ) :
    HasSum (fun k : ℕ => (x + (k : ℂ) * (n : ℂ)) ^ k /
        ((Nat.factorial k : ℂ) * Complex.exp ((k : ℂ) * (n : ℂ))))
      (Complex.exp x / (1 - (n : ℂ)))

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, Corollary 1, formula (16.6), printed pp. 80--81 / PDF pp. 90--91.

Used by 1

Used byRamanujan's \(\psi\)-series (Chapter 3, Entry 16)

TheoremRamanujan's \(\psi\)-series (Chapter 3, Entry 16)#✓fully proved

For natural numbers \(r\), \(k\) and a complex number \(n\) define \(\psi(r, k, n)\) recursively by \(\psi(0, 1, n) = 1\), \(\psi(0, k, n) = 0\) for \(k \ne 1\), and

\[\psi(r + 1, k, n) = (n - r - k)\, \psi(r, k, n) + (r + k - 1)\, \psi(r, k - 1, n),\]

where the last term is read as \(0\) when \(k = 0\). Let \(r\) be a natural number and let \(n\), \(u\) be complex numbers with \(|u e^{1-u}| < 1\) and \(|u| < 1\). Then the series

\[\sum_{j=0}^{\infty} \frac{(n + j)^{r+j}\, e^{-u(n+j)}\, u^j}{j!}\]

converges unconditionally to

\[\sum_{k=1}^{r+1} \frac{\psi(r, k, n)}{(1 - u)^{r+k}}.\]

The hypothesis \(|u| < 1\) selects the component of \(\{u : |u e^{1-u}| < 1\}\) containing \(0\); given \(|u e^{1-u}| < 1\), it is equivalent to \(\operatorname{Re} u < 1\). On the other component the series converges to a different value.

Proof: Entry 12 gives absolute and locally uniform convergence, and termwise differentiation gives the recurrence in Berndt (16.4)-(16.5). The Jensen-series base case from Berndt (16.6) extends to the star-convex domain by analytic uniqueness.

theorem ramanujan_part1_ch3_entry16_psi_series (r : ℕ)
    (n u : ℂ) (h : ‖u * Complex.exp (1 - u)‖ < 1) (hu : ‖u‖ < 1) :
    HasSum (fun j : ℕ => (n + (↑j : ℂ)) ^ (r + j) * Complex.exp (-u * (n + (↑j : ℂ))) * u ^ j /
        (↑(Nat.factorial j) : ℂ)) (∑ k ∈ Finset.Icc 1 (r + 1), psi r k n / (1 - u) ^ (r + k))

def psi : ℕ → ℕ → ℂ → ℂ
  | 0, 1, _ => 1
  | 0, _, _ => 0
  | r + 1, k, n =>
      (n - (↑(r + 1) : ℂ) - (↑k : ℂ) + 1) * psi r k n +
        ((↑(r + 1) : ℂ) + (↑k : ℂ) - 2) * if k = 0 then 0 else psi r (k - 1) n

MathlibExt/NumberTheory/Ramanujan/Part1Ch3Entry16PsiSeries.lean:64

Sources

Berndt, Ramanujan's Notebooks Part I, Chapter 3, construction and formulas (16.4)-(16.5), printed pp. 78-79 / PDF pp. 88-89.

Uses 2

Proof usesAbsolute convergence of the shifted series in Entry 12 for every \(n\) · Jensen's series (Chapter 3, Entry 16, Corollary 1)

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.