Duality, weak topologies and reflexivity

Hahn–Banach, annihilators and bipolars, weak and weak-star convergence and topologies, Goldstine, James, Eberlein–Šmulian, Krein–Šmulian, Banach–Alaoglu, Mazur's lemma, Banach limits, Hamel bases and discontinuous functionals, F-spaces and locally convex spaces, Choquet theory.

TheoremGoldstine's theorem#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), let \(E^{**}\) be its bidual and let \(J : E \to E^{**}\) be the canonical embedding. In the weak-star topology of \(E^{**}\), the closure of the image under \(J\) of the closed unit ball of \(E\) is exactly the closed unit ball of \(E^{**}\).

theorem goldstine
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
    closure
        ((StrongDual.toWeakDual ∘ NormedSpace.inclusionInDoubleDual 𝕜 E) ''
          Metric.closedBall (0 : E) 1)
      = WeakDual.toStrongDual ⁻¹' Metric.closedBall
          (0 : StrongDual 𝕜 (StrongDual 𝕜 E)) 1
Sources
  • H. H. Goldstine, Weakly complete Banach spaces, Duke Math. J. 4 (1938), DOI 10.1215/S0012-7094-38-00410-7; Rudin, Functional Analysis, 2nd ed.; Lean states RCLike field case with metric closedBall formulation.
Used by 2
Used byFinite-coordinate Goldstine theorem · Milman–Pettis theorem

TheoremContinuous linear functionals on the space of all real functions#●ready to prove

Let \(H\) be a set and give the space \(\mathbb{R}^H\) of all real-valued functions on \(H\) the topology of pointwise convergence. Then for every continuous linear functional \(f \colon \mathbb{R}^H \to \mathbb{R}\) there are a natural number \(n\), points \(t_1, \dots, t_n \in H\) and real numbers \(\alpha_1, \dots, \alpha_n\) such that \(f(x) = \sum_{i=1}^n \alpha_i \, x(t_i)\) for every \(x \in \mathbb{R}^H\).

Continuity is the intended reading of the typescript, whose statement prints no continuity hypothesis. Without continuity the claim is false: when \(H\) is infinite, the algebraic dual of \(\mathbb{R}^H\) is strictly larger than the span of the evaluations.

theorem_wanted continuousLinearFunctionalFiniteEvaluations :
    ∀ (H : Type) (f : (H → ℝ) →ₗ[ℝ] ℝ), Continuous f →
      ∃ (n : ℕ) (t : Fin n → H) (α : Fin n → ℝ), ∀ x : H → ℝ,
        f x = ∑ i, α i * x (t i)
Sources
  • S. Banach and S. Mazur, Problem 10 of the Scottish Book, stated as a theorem in the Scottish Book typescript.

TheoremEberlein–Šmulian theorem#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). A subset of \(E\) is compact in the weak topology if and only if it is sequentially compact in the weak topology, that is, every sequence in it has a subsequence that converges weakly to a point of the subset.

theorem eberlein_smulian
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    {s : Set (WeakSpace 𝕜 E)} :
    IsCompact s ↔ IsSeqCompact s
Sources
  • W. F. Eberlein, Weak Compactness in Banach Spaces, PNAS 33 (1947), 51–53, DOI 10.1073/pnas.33.3.51, and V. Smulian (1947); Dunford-Schwartz, Linear Operators I, 1958, V.5-6; Lean states RCLike Banach case with IsCompact ↔ IsSeqCompact in WeakSpace.
Used by 2
Used byDunford–Pettis weak compactness criterion · Banach–Saks theorem for uniformly convex spaces

TheoremDunford–Pettis weak compactness criterion#✓fully proved

Let \(\mu\) be a finite measure on a measurable space \(\alpha\) and let \((f_i)_{i \in \iota}\) be a family of integrable real functions on \(\alpha\). The family is uniformly integrable, meaning that it is bounded in \(L^1(\mu)\) and that for every \(\varepsilon > 0\) there is \(\delta > 0\) with \(\int_s |f_i| \, d\mu \le \varepsilon\) for every \(i\) and every measurable set \(s\) with \(\mu(s) \le \delta\), if and only if the closure of the set of classes \(\{[f_i] : i \in \iota\}\) in the weak topology of \(L^1(\mu)\) is weakly compact.

public theorem dunford_pettis_compactness
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]
    {ι : Type*} (f : ι → α → ℝ) (hf : ∀ i, MemLp (f i) 1 μ) :
    UniformIntegrable f (1 : ℝ≥0∞) μ ↔
      IsCompact
        (closure
          (toWeakSpace ℝ (Lp ℝ 1 μ) '' Set.range (fun i => (hf i).toLp (f i))
            : Set (WeakSpace ℝ (Lp ℝ 1 μ))))
Sources
  • N. Dunford and B. J. Pettis, Linear Operations on Summable Functions, Trans. Amer. Math. Soc. 47 (1940), 323–392, DOI 10.1090/S0002-9947-1940-0002020-4, criterion for weak compactness in L¹; Dunford-Schwartz IV; Lean states finite-measure real L¹ specialization with weak-space closure characterization.
Uses 2
Proof usesEberlein–Šmulian theorem · Milman–Pettis theorem

TheoremExistence of Banach limits#✓fully proved

There is a continuous linear functional \(L\) on the real Banach space \(\ell^\infty\) of bounded real sequences with the supremum norm such that \(L(f) \ge 0\) whenever \(f_n \ge 0\) for every \(n\), \(L\) maps the constant sequence \(1\) to \(1\), \(L(f) = L(g)\) whenever \(g_n = f_{n+1}\) for every \(n\), and \(L(f) = l\) whenever the sequence \(f_n\) converges to \(l\).

public theorem banach_limit :
    ∃ L : BoundedContinuousFunction ℕ ℝ →L[ℝ] ℝ,
      (∀ f : BoundedContinuousFunction ℕ ℝ, (∀ n, 0 ≤ f n) → 0 ≤ L f) ∧
      L (BoundedContinuousFunction.const ℕ (1 : ℝ)) = 1 ∧
      (∀ (f g : BoundedContinuousFunction ℕ ℝ), (∀ n, g n = f (n + 1)) → L f = L g) ∧
      (∀ (f : BoundedContinuousFunction ℕ ℝ) (l : ℝ),
        Filter.Tendsto (fun n => f n) Filter.atTop (nhds l) → L f = l)
Sources
  • S. Banach, Theorie des operations lineaires, 1932, definition of generalised limit; G. Lorentz, Acta Math. 80 (1948) 167-190; Lean formalizes ℓ∞ via BoundedContinuousFunction ℕ ℝ and real field ℝ with all four classical axioms.
Used by 1
Used byJosefson–Nissenzweig theorem

TheoremJosefson–Nissenzweig theorem#✓fully proved

Let \(E\) be an infinite-dimensional Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Then there is a sequence \((\varphi_n)_{n \in \mathbb{N}}\) of continuous linear functionals on \(E\) with \(\|\varphi_n\| = 1\) for every \(n\) such that \(\varphi_n(x) \to 0\) for every \(x \in E\); that is, the unit sphere of the dual of \(E\) contains a weak-star null sequence.

Proof: We apply Rosenthal's ℓ¹ dichotomy to a separated dual sequence, then use the stable-block and Banach-limit/Rademacher route of Hagler--Johnson (1977) and Behrends (1995).

theorem josefson_nissenzweig
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    (hInf : ¬ FiniteDimensional 𝕜 E) :
    ∃ (φ : ℕ → StrongDual 𝕜 E), (∀ n, ‖φ n‖ = 1) ∧
      ∀ x : E, Filter.Tendsto (fun n => (φ n) x) Filter.atTop (nhds (0 : 𝕜))
Sources
  • B. Josefson, Weak sequential convergence in the dual of a Banach space does not imply norm convergence, Bull. Amer. Math. Soc. 81 (1975), 166–168, DOI 10.1090/S0002-9904-1975-13691-3; and A. Nissenzweig, w* sequential convergence, Israel J. Math. 22 (1975), 266–272, DOI 10.1007/BF02761594, Josefson-Nissenzweig theorem; Diestel, Sequences and Series; Lean states RCLike infinite-dimensional Banach case with ‖φ n‖=1 and pointwise weak-star nullness.
Uses 3
Proof usesExistence of Banach limits · Uniform \(\ell^1\) lower bound · Rosenthal's \(\ell^1\) theorem

TheoremKrein–Smulian theorem#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), and let \(C\) be a subset of its dual \(E^*\) that is convex over \(\mathbb{R}\). Then \(C\) is weak-star closed if and only if, for every \(r > 0\), the set \(\{\varphi \in C : \|\varphi\| \le r\}\) is weak-star closed.

theorem krein_smulian
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    {s : Set (WeakDual 𝕜 E)} (hs : Convex ℝ s) :
    IsClosed s ↔
      ∀ (r : ℝ) (_ : 0 < r),
        IsClosed
          (s ∩ WeakDual.toStrongDual ⁻¹' Metric.closedBall (0 : StrongDual 𝕜 E) r)
Sources
  • M. Krein and V. Smulian, Ann. of Math. 41 (1940) 556-583; Dunford-Schwartz I; Lean states RCLike Banach case with Convex ℝ s and closedBall intersections.

TheoremMazur's Problem 24: additive functionals measurable along curves are continuous#●ready to prove

Let \(E\) be a real Banach space and let \(F \colon E \to \mathbb{R}\) be additive, that is, \(F(x + y) = F(x) + F(y)\) for all \(x, y \in E\). If for every continuous map \(x \colon [0, 1] \to E\) the function \(t \mapsto F(x(t))\) on \([0, 1]\) is Borel measurable, then \(F\) is continuous.

theorem_wanted additiveFunctionalMeasurableOnCurvesContinuous :
    ∀ (E : Type) [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
      (F : E → ℝ), (∀ x y, F (x + y) = F x + F y) →
      (∀ (x : C(↥(Set.Icc (0 : ℝ) 1), E)), Measurable fun t => F (x t)) →
      Continuous F
Sources
  • S. Mazur, Problem 24 of the Scottish Book (prize: two small beers). Solved affirmatively by I. Labuda and R. D. Mauldin, "Problem 24 of the Scottish Book concerning additive functionals", Colloquium Mathematicum 48, as quoted in Ger (2016); the proof covers additive operators into a Hausdorff topological vector space.

TheoremNearest points in reflexive Banach spaces#●ready to prove

Let \(X\) be a reflexive complex Banach space, that is, the canonical embedding of \(X\) into its double dual is surjective, and let \(C \subseteq X\) be a nonempty closed convex set. Then for every \(x_0 \in X\) there is \(y_0 \in C\) such that \(\|x_0 - y_0\| = \inf_{y \in C} \|x_0 - y\|\).

public theorem_wanted exists_norm_sub_eq_iInf_of_reflexive_of_convex_of_isClosed
  (X : Type*) [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
  (hX_reflexive : Function.Surjective (NormedSpace.inclusionInDoubleDual ℂ X)) (C : Set X)
  (hC_closed : IsClosed C) (_hC_convex : Convex ℝ C) (hC_nonempty : C.Nonempty) :
  ∀ x₀ : X, ∃ y₀ ∈ C, ‖x₀ - y₀‖ = ⨅ y : C, ‖x₀ - (y : X)‖
Sources
  • MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Normed linear spaces and Banach spaces; Banach lattices), problem ma_proofbench_l2_64.

TheoremPrinciple of local reflexivity#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with dual \(E^*\), bidual \(E^{**}\) and canonical embedding \(J \colon E \to E^{**}\). Let \(M\) and \(N\) be finite-dimensional normed spaces over \(\mathbb{K}\) with injective bounded linear maps \(i_M \colon M \to E^{**}\) and \(i_N \colon N \to E^*\), and let \(\varepsilon > 0\). Then there is a bounded linear map \(T \colon M \to E\) such that for all \(m \in M\), \(n \in N\) and \(x \in E\) we have \((1 + \varepsilon)^{-1} \|i_M(m)\| \le \|T m\| \le (1 + \varepsilon) \|i_M(m)\|\), \(i_N(n)(T m) = i_M(m)(i_N(n))\), and \(T m = x\) whenever \(i_M(m) = J x\).

Proof: Helly's lemma applied to finitely many linear conditions plus one norm bound, then a finite \(\delta\)-net of the unit sphere of \(i_M(M)\) turns net-point bounds into the \((1+\varepsilon)\) bounds (the elementary proof in Albiac–Kalton, Topics in Banach Space Theory).

public theorem principle_of_local_reflexivity
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    {M : Type*} [NormedAddCommGroup M] [NormedSpace 𝕜 M] [FiniteDimensional 𝕜 M]
    {N : Type*} [NormedAddCommGroup N] [NormedSpace 𝕜 N] [FiniteDimensional 𝕜 N]
    (iM : M →L[𝕜] StrongDual 𝕜 (StrongDual 𝕜 E))
    (iN : N →L[𝕜] StrongDual 𝕜 E)
    (hM_inj : Function.Injective iM)
    (hN_inj : Function.Injective iN)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ (T : M →L[𝕜] E),
      (∀ m : M, (1 + ε)⁻¹ * ‖iM m‖ ≤ ‖T m‖ ∧ ‖T m‖ ≤ (1 + ε) * ‖iM m‖)
      ∧ (∀ (m : M) (n : N), (iN n) (T m) = (iM m) (iN n))
      ∧ (∀ (m : M) (x : E), iM m = NormedSpace.inclusionInDoubleDual 𝕜 E x → T m = x)
Sources
  • J. Lindenstrauss and H. Rosenthal, Israel J. Math. 7 (1969) 325-349, principle of local reflexivity; Johnson-Rosenthal-Zippin 1971 refinements; Albiac and Kalton, Topics in Banach Space Theory; Lean states RCLike Banach finite- dimensional M, N version with (1+ε)-isometry and pairing preservation.
7 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.