Summability and Tauberian theorems
Matrix summability methods (Silverman–Toeplitz, Cesàro means, permanent methods) and Tauberian theorems of Tauber, Hardy–Littlewood, Wiener and Newman.
- Cesàro means of random subsequences
- Permanent summability methods
- Tauberian theorems for power series
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
NumberTheoryILemma 16.8.
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))
def HasLaplace (f : ℝ → E) (s : ℂ) (v : E) : Prop :=
LaplaceConvergent f s ∧ laplace f s = v
MathlibExt/Analysis/LaplaceTransform/Basic.lean:50
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.