Classical sequence spaces

ℓ^p and c₀: duality, Schauder bases, compactness criteria, Schur and Rosenthal ℓ¹ theorems, Pitt's theorem, quotients of ℓ¹, finite ℓ^p geometry, convolution on ℓ^p(ℤ).

• Duals of ℓ^p and c₀
• Convolution on ℓ^p(ℤ)
• Geometry of finite-dimensional ℓ^p spaces
• Rosenthal's ℓ¹ theorem
• Schauder basis of ℓ^p
• Compactness in ℓ^p
• Schur's theorem on weak convergence in ℓ¹

TheoremPitt's theorem#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(1 \le q < p < \infty\). Then every bounded linear operator \(T : \ell^p(\mathbb{N}, \mathbb{K}) \to \ell^q(\mathbb{N}, \mathbb{K})\) is compact.

theorem pitt
    {𝕜 : Type*} [RCLike 𝕜]
    (p q : ENNReal) [Fact (1 ≤ p)] [Fact (1 ≤ q)]
    (hq_lt : q < p) (hp_lt : p < ⊤)
    (T : lp (fun _ : ℕ => 𝕜) p →L[𝕜] lp (fun _ : ℕ => 𝕜) q) :
    IsCompactOperator T

Sources

• H. R. Pitt, A Note on Bilinear Forms, J. London Math. Soc. s1-11 (1936), 174–180, DOI 10.1112/JLMS/S1-11.3.174, compactness of operators ℓ^p → ℓ^q for q<p; textbook Albiac and Kalton, Topics in Banach Space Theory Prop 2.1.6; Lean states RCLike lp _ p →L[𝕜] lp _ q with q<p<∞ compact specialization via IsCompactOperator.

TheoremSeparable real Banach spaces are quotients of ℓ¹#✓fully proved

For every separable real Banach space \(E\) there is a surjective bounded linear operator \(T \colon \ell^1(\mathbb{N}, \mathbb{R}) \to E\).

theorem separableRealBanach_quotient_l1
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [TopologicalSpace.SeparableSpace E] :
    ∃ (T : lp (fun _ : ℕ => ℝ) 1 →L[ℝ] E), Function.Surjective T

Sources

• S. Banach, Theorie des operations lineaires, 1932, ℓ¹ quotient theorem; Albiac and Kalton, Topics in Banach Space Theory; Lean states separable real Banach specialization with concrete lp _ 1 domain and surjective bounded linear quotient.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.