James' reflexivity theorem

TheoremFinite-coordinate Goldstine theorem#✓fully proved

Let \(X\) be a real normed space, write \(X^*\) for its dual space of continuous linear functionals and \(X^{**}\) for the dual of \(X^*\), and let \(T \in X^{**}\) with \(\|T\| \le 1\). Then for every finite set \(s \subseteq X^*\) and every real \(\varepsilon > 0\) there is \(x \in X\) with \(\|x\| \le 1\) such that \(|z(x) - T(z)| < \varepsilon\) for every \(z \in s\).

theorem _root_.NormedSpace.goldstine_finite
    {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    (T : StrongDual ℝ (StrongDual ℝ X)) (hT : ‖T‖ ≤ 1)
    (s : Finset (StrongDual ℝ X)) {ε : ℝ} (hε : 0 < ε) :
    ∃ x : X, ‖x‖ ≤ 1 ∧ ∀ z ∈ s, |z x - T z| < ε

Uses 1 · Used by 1

Proof usesGoldstine's theorem

Used byJames' reflexivity theorem

TheoremJames' reflexivity theorem#✓fully proved

Let \(\mathbb{K}\) be \(\mathbb{R}\) or \(\mathbb{C}\) and let \(E\) be a Banach space over \(\mathbb{K}\). The canonical embedding of \(E\) into its bidual \(E^{**}\) is surjective if and only if every continuous linear functional \(f \colon E \to \mathbb{K}\) attains its norm on the closed unit ball, that is, there is \(x \in E\) with \(\|x\| \le 1\) and \(|f(x)| = \|f\|\).

Proof: The reverse implication uses the general real James convex-block argument, with Goldstine approximation and weak-star cluster hulls. Restriction of scalars transfers the result from real scalars to \(\mathbb{K}\).

theorem james_reflexivity
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] :
    Function.Surjective (NormedSpace.inclusionInDoubleDual 𝕜 E)
      ↔ ∀ f : StrongDual 𝕜 E, ∃ x ∈ Metric.closedBall (0 : E) 1, ‖f x‖ = ‖f‖

Sources

• R. C. James, Reflexivity and the Supremum of Linear Functionals, Ann. of Math. 66 (1957), DOI 10.2307/1970122; Bourbaki form; Lean states RCLike Banach case with norm-attainment equivalence for reflexivity.

Uses 1

Proof usesFinite-coordinate Goldstine theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.