Rosenthal's ℓ¹ theorem

DefinitionUniform \(\ell^1\) lower bound#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). A sequence \((y_i)_{i \in \mathbb{N}}\) in \(E\) has a uniform \(\ell^1\) lower bound when there is a real \(c > 0\) such that \(\|\sum_i a_i y_i\| \ge c \sum_i |a_i|\) for every finitely supported sequence \((a_i)_{i \in \mathbb{N}}\) of scalars in \(\mathbb{K}\), both sums running over the finitely many \(i\) with \(a_i \ne 0\).

def HasUniformL1LowerBound {𝕜 E : Type*} [RCLike 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] (y : ℕ → E) : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∀ (a : ℕ →₀ 𝕜),
    ‖∑ i ∈ a.support, a i • y i‖ ≥ c * ∑ i ∈ a.support, ‖a i‖

Used by 2

Used byJosefson–Nissenzweig theorem · Rosenthal's \(\ell^1\) theorem

TheoremRosenthal's \(\ell^1\) theorem#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\) and let \((x_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(E\). Then there is a strictly increasing \(\varphi : \mathbb{N} \to \mathbb{N}\) such that either the subsequence \((x_{\varphi(n)})_{n \in \mathbb{N}}\) is weakly Cauchy, that is, for every continuous linear functional \(f : E \to \mathbb{K}\) and every real \(\varepsilon > 0\) there is \(N\) with \(|f(x_{\varphi(m)}) - f(x_{\varphi(n)})| < \varepsilon\) for all \(m, n \ge N\), or \((x_{\varphi(n)})_{n \in \mathbb{N}}\) has a uniform \(\ell^1\) lower bound.

Proof: We use the Nash-Williams/Galvin-Prikry Ramsey route, following Rosenthal's 1974 theorem, Albiac and Kalton, Sections 10.1–10.2, and Farahat's 1974 proof.

public theorem rosenthal_l1
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    (x : ℕ → E) (hx : Bornology.IsBounded (Set.range x)) :
    ∃ (φ : ℕ → ℕ) (_ : StrictMono φ),
      (∀ (f : E →L[𝕜] 𝕜) (ε : ℝ), 0 < ε →
        ∃ N, ∀ m n, N ≤ m → N ≤ n → ‖f (x (φ m)) - f (x (φ n))‖ < ε) ∨
      HasUniformL1LowerBound (𝕜 := 𝕜) (x ∘ φ)

Sources

• H. P. Rosenthal, A Characterization of Banach Spaces Containing l1, PNAS 71 (1974), 2411–2413, DOI 10.1073/pnas.71.6.2411, ℓ¹ dichotomy theorem; Bourgain et al., extensions; Lean states RCLike Banach bounded Set.range dichotomy with StrictMono φ and HasUniformL1LowerBound defined via ℕ →₀ 𝕜 finitely supported coefficients.

Uses 1 · Used by 1

Statement usesUniform \(\ell^1\) lower bound

Used byJosefson–Nissenzweig theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.