Geometry of Banach spaces

Convexity and smoothness of norms (uniform convexity, Kadec–Klee, Birkhoff–James), extreme points of balls, Auerbach and Schauder bases, approximation property, isometries (Banach–Stone, Mazur–Ulam), Banach–Mazur, Dvoretzky–Rogers, Grothendieck, Rademacher type, Daugavet, Bishop–Phelps.

TheoremBanach–Mazur embedding theorem#✓fully proved

Every separable real Banach space \(E\) admits a linear isometric embedding \(e \colon E \to C([0, 1], \mathbb{R})\) into the space of continuous real functions on \([0, 1]\) with the supremum norm, such that the range of \(e\) is closed.

theorem banachMazur_embedding
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    [TopologicalSpace.SeparableSpace E] :
    ∃ (e : E →ₗᵢ[ℝ] C(Set.Icc (0:ℝ) 1, ℝ)), IsClosed
        (Set.range (e : E → C(Set.Icc (0:ℝ) 1, ℝ)))
Sources
  • S. Banach and S. Mazur 1932 embedding theorem; Banach, Theorie des operations lineaires; Henson-Michalewski, separable Banach as universal space; Lean states separable real Banach case with E →ₗᵢ[ℝ] C(Icc 0 1, ℝ) and IsClosed (range).

TheoremBanach–Stone theorem for real scalars#✓fully proved

Let \(X\) and \(Y\) be compact Hausdorff spaces, and let \(C(X, \mathbb{R})\) and \(C(Y, \mathbb{R})\) be the real Banach spaces of continuous real functions on them with the supremum norm. If there is a surjective linear isometry from \(C(X, \mathbb{R})\) onto \(C(Y, \mathbb{R})\), then \(X\) and \(Y\) are homeomorphic.

theorem banachStone_real
    {X Y : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [TopologicalSpace Y] [CompactSpace Y] [T2Space Y]
    (e : C(X, ℝ) ≃ₗᵢ[ℝ] C(Y, ℝ)) : Nonempty (X ≃ₜ Y)
Sources
  • S. Banach, Theorie des operations lineaires, 1932 and M. Stone, Trans. Amer. Math. Soc. 41 (1937) 375-381; textbook Semadeni, Banach Spaces of Continuous Functions, 1971; Lean states compact Hausdorff case with Banach-space linear isometric isomorphism implies homeomorphism, real coefficient field specialization.

TheoremBishop–Phelps theorem#✓fully proved

Let \(E\) be a Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), with dual space \(E^*\). The functionals that attain their norm on the closed unit ball, that is, the \(f \in E^*\) such that \(|f(x)| = \|f\|\) for some \(x \in E\) with \(\|x\| \le 1\), form a dense subset of \(E^*\) in the norm topology.

theorem bishop_phelps
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] :
    Dense { f : StrongDual 𝕜 E | ∃ x ∈ Metric.closedBall (0 : E) 1, ‖f x‖ = ‖f‖ }
Sources
  • E. Bishop and R. R. Phelps, Bull. Amer. Math. Soc. 67 (1961) 97-98 and Pacific J. Math. 1961; Bollobas quantitative version; Lean states RCLike Banach case as density of attaining functionals.

TheoremDaugavet's theorem for compact operators#✓fully proved

Let \(C[0,1]\) be the real Banach space of continuous functions \([0,1] \to \mathbb{R}\) with the supremum norm, and let \(I\) be the identity operator on it. Every compact bounded linear operator \(T : C[0,1] \to C[0,1]\) satisfies \(\|I + T\| = 1 + \|T\|\), where the norms are operator norms.

theorem daugavet
    (T : C(Set.Icc (0 : ℝ) 1, ℝ) →L[ℝ] C(Set.Icc (0 : ℝ) 1, ℝ))
    (hT : IsCompactOperator T) :
    ‖ContinuousLinearMap.id ℝ C(Set.Icc (0 : ℝ) 1, ℝ) + T‖ = 1 + ‖T‖
Sources
  • I. K. Daugavet, Izv. Vyssh. Uchebn. Zaved. Matematika 1963; Kadets et al., 1980s Daugavet property; Werner, Recent progress on Daugavet property, 2001; Lean states C(Icc 0 1, ℝ) compact-operator specialization of the general Daugavet property ‖Id+T‖=1+‖T‖.

TheoremDvoretzky–Rogers theorem#●ready to prove

Every infinite-dimensional real Banach space \(E\) contains a series that converges unconditionally but not absolutely: there is a sequence \((x_n)_{n \ge 0}\) in \(E\) such that the rearranged series \(\sum_n x_{\sigma(n)}\) converges for every permutation \(\sigma\) of \(\mathbb{N}\), while \(\sum_n \lVert x_n \rVert\) diverges.

theorem_wanted dvoretzky_rogers_unconditional_not_absolute :
    ∀ (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E],
      ¬ Module.Finite ℝ E →
      ∃ x : ℕ → E,
        (∀ σ : Equiv.Perm ℕ, Summable (x ∘ σ)) ∧
        ¬ Summable (fun n => ‖x n‖)
Sources
  • S. Mazur and W. Orlicz, Problem 122 of the Scottish Book; A. Dvoretzky and C. A. Rogers, "Absolute and unconditional convergence in normed linear spaces", Proc. Natl. Acad. Sci. USA 36 (1950), 192-197.

TheoremGrothendieck's inequality (real case)#✓fully proved

There is a constant \(K > 0\) such that for all \(m, n \in \mathbb{N}\), every real \(m \times n\) matrix \(A = (a_{ij})\), every real Hilbert space \(H\) and all vectors \(x_1, \dots, x_m, y_1, \dots, y_n \in H\) of norm at most \(1\), there are signs \(\varepsilon_1, \dots, \varepsilon_m, \delta_1, \dots, \delta_n \in \{1, -1\}\) such that \(\bigl|\sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \langle x_i, y_j \rangle\bigr| \le K \bigl|\sum_{i=1}^{m} \sum_{j=1}^{n} a_{ij} \varepsilon_i \delta_j\bigr|\).

theorem grothendieck_inequality_real :
    ∃ K : ℝ, 0 < K ∧
      ∀ (m n : ℕ) (A : Matrix (Fin m) (Fin n) ℝ)
        (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
        (x : Fin m → H) (y : Fin n → H),
        (∀ i, ‖x i‖ ≤ 1) → (∀ j, ‖y j‖ ≤ 1) →
        ∃ (ε : Fin m → ℝ) (δ : Fin n → ℝ),
          (∀ i, ε i = 1 ∨ ε i = -1) ∧
          (∀ j, δ j = 1 ∨ δ j = -1) ∧
          |∑ i : Fin m, ∑ j : Fin n, A i j * ⟪x i, y j⟫_ℝ| ≤
            K * |∑ i : Fin m, ∑ j : Fin n, A i j * ε i * δ j|
Sources
  • A. Grothendieck, Resume de la theorie metrique des produits tensoriels topologiques, Bol. Soc. Mat. Sao Paulo 8 (1953) 1-79, inequality; Pisier, Grothendieck's theorem past and present, 2012; Lean states real finite-matrix scalarized form with Fin-indexed unit vectors and ±1 signs, existential universal constant K.

TheoremMilman–Pettis theorem#✓fully proved

Let \(E\) be a uniformly convex Banach space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\), and let \(E^*\) be the space of continuous linear functionals on \(E\). Then every continuous linear functional \(\Phi\) on \(E^*\) is evaluation at a point: there is \(x \in E\) with \(\Phi(f) = f(x)\) for every \(f \in E^*\).

theorem milman_pettis
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [UniformConvexSpace E] [CompleteSpace E]
    (Φ : (E →L[𝕜] 𝕜) →L[𝕜] 𝕜) :
    ∃ x : E, ∀ (f : E →L[𝕜] 𝕜), Φ f = f x
Sources
  • D. Milman, C. R. (Doklady) Acad. Sci. URSS 18 (1938) and B. Pettis, Duke Math. J. 1939, Milman-Pettis theorem that uniformly convex Banach spaces are reflexive; Clarkson uniform convexity 1936; Lean states RCLike uniformly convex complete case via double-dual evaluation surjectivity.
Uses 1 · Used by 2
Proof usesGoldstine's theorem
Used byDunford–Pettis weak compactness criterion · Banach–Saks theorem for uniformly convex spaces

TheoremBanach–Saks theorem for uniformly convex spaces#✓fully proved

Let \(E\) be a uniformly convex real Banach space and let \((x_n)_{n \in \mathbb{N}}\) be a bounded sequence in \(E\). Then there are a strictly increasing map \(\varphi : \mathbb{N} \to \mathbb{N}\) and a point \(y \in E\) such that the Cesàro means \(\frac{1}{n} \sum_{i=0}^{n-1} x_{\varphi(i)}\) converge to \(y\) in norm as \(n \to \infty\).

public theorem banach_saks
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E] [CompleteSpace E]
    {x : ℕ → E} (hx : Bornology.IsBounded (Set.range x)) :
    ∃ (φ : ℕ → ℕ) (_ : StrictMono φ) (y : E),
      Filter.Tendsto (fun n : ℕ => (n : ℝ)⁻¹ • ∑ i ∈ Finset.range n, x (φ i)) Filter.atTop (nhds y)
Sources
  • S. Banach and S. Saks, Studia Math. 2 (1930) 51-57; uniformly convex form and property due to Kakutani, 1939; textbook Diestel, Sequences and Series in Banach Spaces; Lean gives uniformly convex real Banach specialization with explicit StrictMono φ and norm-convergent Cesàro means.
Uses 2
Proof usesEberlein–Šmulian theorem · Milman–Pettis theorem
7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.