Summability and Tauberian theorems

Matrix summability methods (Silverman–Toeplitz, Cesàro means, permanent methods) and Tauberian theorems of Tauber, Hardy–Littlewood, Wiener and Newman.

TheoremIntegral criterion for asymptotic equivalence to the identity#✓fully proved

Let \(f\) be a real function on \(\mathbb{R}\) that is nondecreasing on \([1, \infty)\), and suppose that the integral \(\int_1^x (f(t) - t) / t^2 \, dt\) converges to a finite limit as \(x \to \infty\). Then \(f(x) \sim x\) as \(x \to \infty\).

No monotonicity is assumed below \(1\).

theorem isEquivalent_id_of_monotoneOn_of_tendsto_integral_sub_div_sq
    (f : ℝ → ℝ) (hf : MonotoneOn f (Ici 1))
    (hconv : ∃ L : ℝ,
      Tendsto (fun x => ∫ t in Ioc 1 x, (f t - t) / t ^ 2)
        atTop (𝓝 L)) :
    f ~[atTop] (fun x : ℝ => x)
Sources
  • ATLAS NumberTheoryI Lemma 16.8.
Used by 2

TheoremNewman's Tauberian theorem#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{C}\) be almost everywhere strongly measurable on \((0, \infty)\) and bounded on \([0, \infty)\): for some real \(B \ge 0\), \(|f(t)| \le B\) for all \(t \ge 0\). Let \(G : \mathbb{C} \to \mathbb{C}\) be analytic at every point of the closed half-plane \(\{s : \operatorname{Re} s \ge 0\}\), and suppose that for every \(s\) with \(\operatorname{Re} s > 0\) the Laplace transform of \(f\) converges at \(s\) and equals \(G(s)\). Then \(\int_0^T f(t)\,dt \to G(0)\) as \(T \to \infty\).

theorem newman_tauberian (f : ℝ → ℂ) (B : ℝ)
    (hfmeas : AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)))
    (hB : 0 ≤ B) (hbound : ∀ t : ℝ, 0 ≤ t → ‖f t‖ ≤ B)
    (G : ℂ → ℂ)
    (hG_analytic : AnalyticOnNhd ℂ G {s | 0 ≤ s.re})
    (hG : ∀ s : ℂ, 0 < s.re → HasLaplace f s (G s)) :
    Filter.Tendsto (fun T : ℝ => ∫ t : ℝ in (0 : ℝ)..T, f t)
      Filter.atTop (𝓝 (G 0))
Uses 5 · Used by 3

TheoremSilverman–Toeplitz theorem (sufficiency)#✓fully proved

Let \((a_{nk})_{n, k \ge 0}\) be an infinite matrix of complex numbers. Suppose that there is a real \(C\) such that for every \(n\) the series \(\sum_k |a_{nk}|\) converges with sum at most \(C\), that \(a_{nk} \to 0\) as \(n \to \infty\) for every \(k\), and that \(\sum_k a_{nk} \to 1\) as \(n \to \infty\). Then for every sequence \((x_k)\) of complex numbers converging to \(L\), the series \(\sum_k a_{nk} x_k\) converges absolutely for every \(n\), and \(\sum_k a_{nk} x_k \to L\) as \(n \to \infty\).

theorem silverman_toeplitz (A : ℕ → ℕ → ℂ)
    (h_bdd : ∃ C : ℝ, ∀ n, Summable (fun k => ‖A n k‖) ∧
      ∑' k, ‖A n k‖ ≤ C)
    (h_col : ∀ k, Filter.Tendsto (fun n => A n k) Filter.atTop (nhds 0))
    (h_sum : Filter.Tendsto (fun n => ∑' k, A n k) Filter.atTop (nhds 1)) :
    ∀ (x : ℕ → ℂ) (L : ℂ), Filter.Tendsto x Filter.atTop (nhds L) →
      (∀ n, Summable (fun k => A n k * x k)) ∧
        Filter.Tendsto (fun n => ∑' k, A n k * x k) Filter.atTop (nhds L)
Sources
  • https://en.wikipedia.org/wiki/Silverman%E2%80%93Toeplitz_theorem.

TheoremWiener's Tauberian theorem on \(L^1(\mathbb{R})\)#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{C}\) be Lebesgue integrable, and suppose that its Fourier transform \(\hat f(w) = \int_{\mathbb{R}} e^{-2\pi i x w} f(x)\,dx\) vanishes at no real \(w\). Then for every Lebesgue integrable \(g : \mathbb{R} \to \mathbb{C}\) and every \(\varepsilon > 0\) there are a finite set \(S \subset \mathbb{R}\) and coefficients \(c_t \in \mathbb{C}\) for \(t \in S\) such that the function \(h(x) = g(x) - \sum_{t \in S} c_t f(x - t)\) is integrable and \(\int_{\mathbb{R}} |h(x)|\,dx < \varepsilon\). In other words, the translates of \(f\) span a dense subspace of \(L^1(\mathbb{R})\).

theorem wiener_tauberian_L1
    (f : ℝ → ℂ) (hf : Integrable f volume)
    (hF : ∀ w : ℝ, 𝓕 f w ≠ 0) :
    ∀ (g : ℝ → ℂ), Integrable g volume → ∀ ε > 0,
      ∃ (s : Finset ℝ) (c : ℝ → ℂ),
        Integrable (fun x => g x - ∑ t ∈ s, c t * f (x - t)) volume ∧
        ∫ x, ‖g x - ∑ t ∈ s, c t * f (x - t)‖ < ε
Sources
  • N. Wiener, Ann. of Math. 33 (1932) 1–100, DOI 10.2307/1968102, Thm I; Rudin, Fourier Analysis on Groups
Uses 1
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.