Asymptotic analysis

Asymptotic expansions and methods: Euler–Maclaurin and Watson's lemma, Laplace-type integrals, coefficient asymptotics of power series (Bender's lemma), Stirling-type and inverse-factorial expansions, and asymptotic expansions of power sums, Lambert series and log sums; complex-analytic saddle-point results on entire functions go to Complex analysis.

TheoremEuler–Maclaurin formula#✓fully proved

Let \(a < b\) be integers, let \(p \ge 1\) be a natural number, and let \(f : \mathbb{R} \to \mathbb{R}\) be \(p\) times continuously differentiable on \([a, b]\), its derivatives \(f^{(k)}\) being taken relative to \([a, b]\) (one-sided at the endpoints). Let \(B_j\) be the Bernoulli numbers with \(B_1 = -\tfrac{1}{2}\). Then there are \(1\)-periodic functions \(P_m : \mathbb{R} \to \mathbb{R}\) for \(m \ge 0\) such that \(P_p\) agrees on \([0, 1)\) with the Bernoulli polynomial \(\sum_{j=0}^{p} \binom{p}{j} B_j x^{p-j}\), and \(\sum_{n=a}^{b} f(n) = I + E + R\), where \(I = \int_a^b f(x)\,dx + \frac{f(a) + f(b)}{2}\), \(E = \sum_{k=1}^{\lfloor p/2 \rfloor} \frac{B_{2k}}{(2k)!} (f^{(2k-1)}(b) - f^{(2k-1)}(a))\) and \(R = \frac{(-1)^{p+1}}{p!} \int_a^b P_p(x) f^{(p)}(x)\,dx\).

MetaMathlibExt.eulerMaclaurinFormula · 18 lines

theorem eulerMaclaurinFormula :
    ∀ (a b : ℤ) (p : ℕ) (f : ℝ → ℝ),
      a < b →
      1 ≤ p →
      ContDiffOn ℝ (↑p) f (Set.Icc (↑a) (↑b)) →
      ∃ P : ℕ → ℝ → ℝ,
        (∀ (m : ℕ) (x : ℝ), P m (x + 1) = P m x) ∧
        (∀ x ∈ Set.Ico (0 : ℝ) 1, P p x =
          ∑ j ∈ Finset.range (p + 1), (Nat.choose p j : ℝ) *
            (if j = 1 then (-1 / 2 : ℝ) else (bernoulli j : ℝ)) * x ^ (p - j)) ∧
        ∑ n ∈ Finset.Icc a b, f (↑n) =
          (∫ x in (↑a)..(↑b), f x) + (f (↑a) + f (↑b)) / 2 +
            (∑ k ∈ Finset.Icc 1 (p / 2),
              (bernoulli (2 * k) : ℝ) / (Nat.factorial (2 * k) : ℝ) *
                (iteratedDerivWithin (2 * k - 1) f (Set.Icc (↑a) (↑b)) (↑b) -
                  iteratedDerivWithin (2 * k - 1) f (Set.Icc (↑a) (↑b)) (↑a))) +
            ((-1 : ℝ) ^ (p + 1) / (Nat.factorial p : ℝ) *
              (∫ x in (↑a)..(↑b), P p x * iteratedDerivWithin p f (Set.Icc (↑a) (↑b)) x))

Sources

• https://en.wikipedia.org/wiki/Euler%E2%80%93Maclaurin_formula.

Used by 3

Used byRemainder bound for the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Ramanujan's asymptotic expansion of power sums · Ramanujan's asymptotic expansion of a binomial combination of log-power sums

• Asymptotic expansion of Poisson averages
• Asymptotic expansion of the Catalan numbers
• Asymptotic expansions of factorial series
• Asymptotic expansions of Lambert series
• Asymptotic expansions of power sums
• Bender's lemma
• Convolution asymptotics of subexponential functions
• Taylor's law for integer sequences

TheoremWatson's inverse factorial expansion#●ready to prove

Let \(A,B,\rho,\sigma,\alpha,\delta>0\), \(\gamma\ge 0\) and \(p\) be real numbers with \(\alpha+3\delta\lt \pi/2\) and \(1\lt p<1+e^{-\pi\cot\alpha}\). Let \(S\) be the sector \(\{z\in\mathbb{C} : |z|>\gamma,\ |\arg z|\le\pi/2+\alpha+3\delta\}\), where \(\arg\) is the principal argument. Let \(f\) be a complex function that is analytic at every point of the half-plane \(\{z : \mathrm{Re}\,z>0\}\) and at every point of \(S\), let \(a_0,a_1,\dots\) be complex numbers with \(|a_n|\lt A\rho^n n!\) for every \(n\ge 0\), and let \(R_0,R_1,\dots\) be complex functions such that for every \(n\ge 0\) and every \(z\in S\)

\[f(z)=\sum_{k=0}^{n}\frac{a_k}{z^k}+R_n(z)\qquad\text{and}\qquad|R_n(z)\,z^{n+1}|\lt B\sigma^n n!.\]

Suppose that \(M_0\) is the largest real \(x>0\) with

\[e^{-2\cos\alpha/(\rho x)}-2\cos\big(\sin\alpha/(\rho x)\big)e^{-\cos\alpha/(\rho x)}+1-p^2=0.\]

Then for every real \(M\) with \(0\lt M\le M_0\) and every complex \(w\) with \(\mathrm{Re}\,w\ge 0\) there are complex numbers \(b_0,b_1,\dots\) such that for every \(z\) with \(\mathrm{Re}\,z>0\) the series

\[\sum_{k=1}^{\infty}\frac{b_k}{(Mz+w+1)(Mz+w+2)\cdots(Mz+w+k)}\]

converges absolutely and its sum is \(f(z)-b_0\).

MetaMathlibExt.watson_inverse_factorial_series · 35 lines

theorem_wanted watson_inverse_factorial_series
    (f : ℂ → ℂ) (a : ℕ → ℂ) (R : ℕ → ℂ → ℂ)
    (A B ρ σ γ α δ p M₀ : ℝ)
    (hA : 0 < A) (hB : 0 < B) (hρ : 0 < ρ) (hσ : 0 < σ)
    (hγ : 0 ≤ γ) (hα : 0 < α) (hδ : 0 < δ)
    (hangle : α + 3 * δ < Real.pi / 2)
    (hp_lower : 1 < p)
    (hp_upper : p < 1 + Real.exp (-Real.pi * Real.cot α))
    (hanalytic_right : AnalyticOnNhd ℂ f {z : ℂ | 0 < z.re})
    (hanalytic_sector : AnalyticOnNhd ℂ f
      {z : ℂ | γ < ‖z‖ ∧ |Complex.arg z| ≤ Real.pi / 2 + α + 3 * δ})
    (hasymptotic : ∀ n : ℕ, ∀ z : ℂ,
      z ∈ {u : ℂ | γ < ‖u‖ ∧ |Complex.arg u| ≤ Real.pi / 2 + α + 3 * δ} →
      f z = ∑ k ∈ Finset.range (n + 1), a k / z ^ k + R n z)
    (ha_bound : ∀ n : ℕ, ‖a n‖ < A * ρ ^ n * n.factorial)
    (hR_bound : ∀ n : ℕ, ∀ z : ℂ,
      z ∈ {u : ℂ | γ < ‖u‖ ∧ |Complex.arg u| ≤ Real.pi / 2 + α + 3 * δ} →
      ‖R n z * z ^ (n + 1)‖ < B * σ ^ n * n.factorial)
    (hM₀ : IsGreatest
      {x : ℝ | 0 < x ∧
        Real.exp (-(2 * Real.cos α) / (ρ * x)) -
          2 * Real.cos (Real.sin α / (ρ * x)) *
            Real.exp (-Real.cos α / (ρ * x)) + 1 - p ^ 2 = 0} M₀) :
    ∀ M : ℝ, 0 < M → M ≤ M₀ → ∀ w : ℂ, 0 ≤ w.re →
      ∃ b : ℕ → ℂ, ∀ z : ℂ, 0 < z.re →
        Summable (fun k : ℕ =>
          ‖b (k + 1) /
            ∏ j ∈ Finset.range (k + 1),
              ((M : ℂ) * z + w + ((j + 1 : ℕ) : ℂ))‖) ∧
        HasSum
          (fun k : ℕ =>
            b (k + 1) /
              ∏ j ∈ Finset.range (k + 1),
                ((M : ℂ) * z + w + ((j + 1 : ℕ) : ℂ)))
          (f z - b 0)

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL25/Schumacher/schu9.tex, lines 370-417. Scope exclusion: excludes the M = 1, w = 0 specialization and the later Stirling-coefficient theorem.

TheoremWatson's lemma for Laplace integrals#✓fully proved

Let \(g : \mathbb{R} \to \mathbb{R}\) and let \((c_k)_{k \ge 1}\) be real numbers such that for every \(N \ge 0\), \(g(s) - \sum_{k=1}^{N} c_k s^k = O(s^{N+1})\) as \(s \to 0^+\). Suppose there is \(m_0 \in \mathbb{R}\) such that \(s \mapsto g(s) e^{-ms}\) is integrable on \((0, \infty)\) for every \(m \ge m_0\). Then for every \(N \ge 0\), \(\int_0^\infty g(s) e^{-ms} \, ds - \sum_{k=1}^{N} k! \, c_k / m^{k+1} = O(1 / m^{N+2})\) as \(m \to \infty\).

The case \(N = 0\) of the hypothesis says \(g(s) = O(s)\) as \(s \to 0^+\): the expansion of \(g\) has no constant term.

theorem watson_laplace_integral_asymptotic
  (g : ℝ → ℝ) (c : ℕ → ℝ)
  (hlocal : ∀ N : ℕ, Asymptotics.IsBigO (nhdsWithin 0 (Set.Ioi 0))
    (fun s : ℝ => g s - (∑ k ∈ Finset.range N, c (k + 1) * s ^ (k + 1)))
    (fun s : ℝ => s ^ (N + 1)))
  (hconv : ∃ m₀ : ℝ, ∀ m ≥ m₀, MeasureTheory.IntegrableOn
    (fun s : ℝ => g s * Real.exp (-m * s)) (Set.Ioi 0)) :
  ∀ N : ℕ, Asymptotics.IsBigO Filter.atTop
    (fun m : ℝ => (∫ s in Set.Ioi 0, g s * Real.exp (-m * s)) -
      (∑ k ∈ Finset.range N,
        ((Nat.factorial (k + 1) : ℕ) : ℝ) * c (k + 1) / m ^ (k + 2)))
    (fun m : ℝ => 1 / m ^ (N + 2))

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL14/Nemes/nemes4.tex, lines 142-151.

Used by 1

Used byAsymptotic expansion of the Bernoulli numbers of the second kind

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.