Asymptotic expansion of Poisson averages

TheoremLogarithmic asymptotics of the square-root Poisson series#✓fully proved

For real \(x\) let \(S(x) = \sum_{k=1}^{\infty} x^k \sqrt{k} / k!\). Then, as \(x \to \infty\),

\[\log S(x) = x + \tfrac{1}{2} \log x - \frac{1}{8x} - \frac{1}{16 x^2} + O\left(x^{-3}\right).\]
theorem ramanujan_part1_ch3_entry10_example1_sqrt_poisson_asymptotic :
    (fun x : ℝ =>
        Real.log (∑' (j : ℕ), x ^ (j + 1) * Real.sqrt (↑(j + 1) : ℝ) /
            (↑(Nat.factorial (j + 1)) : ℝ)) - (x + (1 / 2 : ℝ) * Real.log x - 1 / (8 * x) - 1 /
                (16 * x ^ 2))) =O[Filter.atTop] (fun x : ℝ =>
            1 / x ^ 3)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 1, printed p. 64 / PDF p. 74.

TheoremEventual summability of the square-root Poisson series#✓fully proved

For all sufficiently large real \(x\), the series \(\sum_{k=1}^{\infty} x^k \sqrt{k} / k!\) is summable.

theorem ramanujan_part1_ch3_entry10_example1_summable_eventually :
    ∀ᶠ (x : ℝ) in Filter.atTop,
        Summable (fun j : ℕ => x ^ (j + 1) * Real.sqrt (↑(j + 1) : ℝ) /
            (↑(Nat.factorial (j + 1)) : ℝ))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 1, printed p. 64 / PDF p. 74.
Used by 1
Used byEventual positivity of the square-root Poisson series

TheoremEventual positivity of the square-root Poisson series#✓fully proved

For all sufficiently large real \(x\), the sum \(\sum_{k=1}^{\infty} x^k \sqrt{k} / k!\) is strictly positive.

theorem ramanujan_part1_ch3_entry10_example1_sum_positive_eventually :
    ∀ᶠ (x : ℝ) in Filter.atTop, 0 < ∑' (j : ℕ), x ^ (j + 1) * Real.sqrt (↑(j + 1)) /
        (↑(Nat.factorial (j + 1)) : ℝ)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 1, printed p. 64 / PDF p. 74.
Uses 1
Proof usesEventual summability of the square-root Poisson series

TheoremAsymptotics of the logarithmic Poisson series#✓fully proved

There are real constants \(C > 0\) and \(x_0\) such that for every real \(x \ge x_0\) the series \(\sum_{k=1}^{\infty} x^k \log(k + 1) / k!\) has a sum \(S\) satisfying

\[\left| e^{-x} S - \log x - \frac{1}{2x} - \frac{1}{12 x^2} \right| \le \frac{C}{x^3}.\]
theorem ramanujan_part1_ch3_entry10_example2_log_poisson_asymptotic :
    ∃ (C : ℝ) (x₀ : ℝ), 0 < C ∧ ∀ (x : ℝ), x₀ ≤ x → ∃ (S : ℝ),
        HasSum (fun j : ℕ => x ^ (j + 1) * Real.log ((j + 2 : ℝ)) / (Nat.factorial (j + 1) : ℝ)) S ∧
            |Real.exp (-x) * S - Real.log x - 1 / (2 * x) - 1 / (12 * x ^ 2)| ≤ C / x ^ 3
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 2, printed p. 65 / PDF p. 75.

TheoremSummability of the logarithmic Poisson series#✓fully proved

For every real \(x\), the series \(\sum_{k=1}^{\infty} e^{-x} x^k \log(k + 1) / k!\) is summable.

theorem ramanujan_part1_ch3_entry10_example2_summable :
    ∀ (x : ℝ),
        Summable (fun j : ℕ => Real.exp (-x) * x ^ (j + 1) * Real.log ((j : ℝ) + 2) /
            (Nat.factorial (j + 1) : ℝ))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 2, printed p. 65 / PDF p. 75.

TheoremSummability of the harmonic Poisson series#✓fully proved

Let \(H_k = \sum_{j=1}^{k} 1/j\) be the \(k\)-th harmonic number (so \(H_0 = 0\)). For every real \(x\), the series \(\sum_{k=0}^{\infty} e^{-x} x^k H_k / k!\) is summable.

theorem ramanujan_part1_ch3_entry10_example4_summable (x : ℝ) :
    Summable (fun k : ℕ => Real.exp (-x) * x ^ k *
        (∑ j ∈ Finset.Icc (1 : ℕ) k, (1 : ℝ) / (j : ℝ)) / (Nat.factorial k : ℝ))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 4, printed pp. 65-66 / PDF pp. 75-76.
Used by 1
Used byAsymptotics of the harmonic Poisson series

TheoremAsymptotics of the harmonic Poisson series#✓fully proved

Let \(H_k = \sum_{j=1}^{k} 1/j\) be the \(k\)-th harmonic number (so \(H_0 = 0\)) and let \(\gamma\) be the Euler–Mascheroni constant. Then, as \(x \to \infty\),

\[e^{-x} \sum_{k=0}^{\infty} \frac{x^k H_k}{k!} = \log x + \gamma + O\left(\frac{1}{x}\right).\]
theorem ramanujan_part1_ch3_entry10_example4_harmonic_poisson_asymptotic :
    Asymptotics.IsBigO Filter.atTop (fun x : ℝ => Real.exp (-x) *
        (∑' (k : ℕ),
            (x ^ k * (∑ j ∈ Finset.Icc 1 k, (1 : ℝ) / (j : ℝ)) /
                (k.factorial : ℝ))) - (Real.log x + Real.eulerMascheroniConstant)) (fun x : ℝ =>
                (1 : ℝ) / x)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, Example 4, printed pp. 65-66 / PDF pp. 75-76.
Uses 1
Proof usesSummability of the harmonic Poisson series

Definition2-associated Stirling numbers in Ramanujan's Entry 10#✓fully proved

For natural numbers \(n\) and \(k\), \(S_2(n, k)\) is the integer \(\sum_{j=0}^{k} (-1)^j \binom{n}{j} S(n - j, k - j)\), where \(S\) denotes the Stirling numbers of the second kind.

\(S_2(n, k)\) is the number of partitions of an \(n\)-element set into \(k\) blocks, each containing at least two elements.

def twoAssocStirlingSecond (n k : ℕ) : ℤ :=
  ∑ j ∈ Finset.range (k + 1), ((-1 : ℤ) ^ j) * (Nat.choose n j : ℤ) *
      (Nat.stirlingSecond (n - j) (k - j) : ℤ)
Used by 2
Used byRamanujan's asymptotic expansion of Poisson averages · The Entry 10 Stirling numbers are the 2-associated Stirling numbers

TheoremThe Entry 10 Stirling numbers are the 2-associated Stirling numbers#✓fully proved

For all natural numbers \(n\) and \(k\), the integer \(\sum_{j=0}^{k} (-1)^j \binom{n}{j} S(n - j, k - j)\) used in Ramanujan's Entry 10, where \(S\) denotes the Stirling numbers of the second kind, equals the 2-associated Stirling number of the second kind \(S_2(n, k)\).

theorem twoAssocStirlingSecond_eq_canonical (n k : ℕ) :
    twoAssocStirlingSecond n k = MetaMathlibExt.twoAssocStirlingSecond n k
Uses 2 · Used by 1
Statement uses2-associated Stirling numbers in Ramanujan's Entry 10 · 2-associated Stirling numbers of the second kind
Used byRamanujan's asymptotic expansion of Poisson averages

TheoremRamanujan's asymptotic expansion of Poisson averages#✓fully proved

Let \(M \ge 1\) be an integer, \(\varphi : \mathbb{R} \to \mathbb{C}\) and \(G : \mathbb{R} \to \mathbb{R}\) functions, \(A \ge 1\) a real number and \(F\) a finite set of natural numbers. Write \(\varphi^{(n)}\) for the \(n\)-th iterated derivative of \(\varphi\) and \(S_2(n, k)\) for the 2-associated Stirling numbers of the second kind. Assume that there are \(C \ge 0\) and \(p \in \mathbb{N}\) such that \(|\varphi(x)| \le C x^p\) and \(|G(x)| \le C x^p\) for all sufficiently large \(x\); that \(G(x) \ge 1\) for all sufficiently large \(x\); and that for every integer \(m \ge 1\) and all sufficiently large \(x\), the derivatives \(\varphi^{(0)}, \dots, \varphi^{(m-1)}\) are differentiable at \(x\) and \(|\varphi^{(m)}(x)| / m! \le G(x) (A / x)^m\). Then, as \(x \to \infty\),

\[e^{-x} \sum_{j \in \mathbb{N} \setminus F} \frac{x^j}{j!} \varphi(j) - \varphi(x) - \sum_{k=2}^{M} \sum_{n=k}^{2k-2} S_2(n, n + 1 - k) \, x^{n-k+1} \frac{\varphi^{(n)}(x)}{n!} = O\left(\frac{G(x)}{x^M}\right).\]

Proof: Taylor expansion on the central Poisson range is combined with the associated-Stirling central-moment identity from Comtet; Berndt's route and even-moment tails control the remainder.

MathlibExt.NumberTheory.Ramanujan.Part1Ch3.Entry10PoissonAsymptotic.ramanujan_part1_ch3_entry10_poisson_asymptotic · 19 lines 
theorem ramanujan_part1_ch3_entry10_poisson_asymptotic
  (M : ℕ) (hM : 0 < M)
  (φ : ℝ → ℂ) (G : ℝ → ℝ) (A : ℝ) (hA : 1 ≤ A)
  (F : Finset ℕ)
  (h_poly : ∃ C : ℝ, 0 ≤ C ∧ ∃ p : ℕ, ∀ᶠ x in Filter.atTop, ‖φ x‖ ≤ C * x ^ p ∧ ‖G x‖ ≤ C * x ^ p)
  (hG_ge : ∀ᶠ x in Filter.atTop, (1 : ℝ) ≤ G x)
  (h_deriv : ∀ m : ℕ, 0 < m → ∀ᶠ x in Filter.atTop,
      (∀ k ∈ Finset.Icc 1 m, DifferentiableAt ℝ (iteratedDeriv (k - 1) φ) x) ∧
          ‖iteratedDeriv m φ x / (Nat.factorial m : ℂ)‖ ≤ G x * (A / x) ^ m) :
    Asymptotics.IsBigO Filter.atTop
    (fun x : ℝ =>
      ((Real.exp (-x) : ℂ)) *
          (∑' j : ℕ, if j ∈ F then (0 : ℂ) else
              (((x ^ j / (Nat.factorial j : ℝ) : ℝ) : ℂ) * φ (j : ℝ)))
      - φ x
      - ∑ k ∈ Finset.Icc 2 M, ∑ n ∈ Finset.Icc k (2 * k - 2),
          (((twoAssocStirlingSecond n (n + 1 - k) : ℤ) : ℂ) * ((x : ℂ) ^ (n - k + 1)) *
              (iteratedDeriv n φ x / (Nat.factorial n : ℂ))))
    (fun x : ℝ => G x / (x : ℝ) ^ M)
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, printed pp. 57-58 / PDF pp. 67-68.
Uses 4
Statement uses2-associated Stirling numbers in Ramanujan's Entry 10
Proof usesThe Entry 10 Stirling numbers are the 2-associated Stirling numbers · 2-associated Stirling numbers of the second kind · Vanishing of 2-associated Stirling numbers of the second kind

TheoremEventual summability of the series in Entry 10#✓fully proved

Let \(\varphi : \mathbb{R} \to \mathbb{C}\) be polynomially bounded at infinity, that is, there are a real number \(C \ge 0\) and a natural number \(p\) such that \(|\varphi(x)| \le C x^p\) for all sufficiently large real \(x\). Let \(F\) be a finite set of natural numbers. Then for all sufficiently large real \(x\), the family indexed by the natural numbers \(j\) whose \(j\)-th term is \(0\) for \(j \in F\) and \(x^j \varphi(j) / j!\) for \(j \notin F\) is summable.

theorem ramanujan_part1_ch3_entry10_poisson_summable
    (φ : ℝ → ℂ) (F : Finset ℕ)
    (hφ : ∃ (C : ℝ) (p : ℕ), 0 ≤ C ∧ ∀ᶠ (x : ℝ) in Filter.atTop, ‖φ x‖ ≤ C * x ^ p) :
    ∀ᶠ (x : ℝ) in Filter.atTop,
      Summable (fun j : ℕ => if j ∈ F then 0 else ((x : ℂ) ^ j * φ (j : ℝ) / (Nat.factorial j : ℂ)))
Sources
  • Berndt, Ramanujan's Notebooks Part I, Chapter 3, Entry 10, printed pp. 57-58 / PDF pp. 67-68.
11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.