Complemented subspacesPaper & formalisation
A mathematical companion

A negative solution to the complemented subspace problem for Banach spaces with unconditional bases

Antonio Acuaviva

This website accompanies the paper and presents the formal verification of its principal results in Lean. Each mathematical statement appears alongside its Lean formulation, with expandable, step-by-step explanations.

Theorem A

Mathematical statement · real field
For every ρ>0\rho>0, there exist sequences (Nj)j=1∞(N_j)_{j=1}^{\infty} in N\mathbb N and (pj)j=1∞(p_j)_{j=1}^{\infty} in (2,3](2,3], with pj↓2p_j\downarrow2, and a projection PρP_\rho on the separable superreflexive real Banach lattice Xρ=(⨁j=1∞ℓpjNj(R))2 X_\rho=\left(\bigoplus_{j=1}^{\infty}\ell_{p_j}^{N_j}(\mathbb R)\right)_2 such that, with Zρ=Pρ(Xρ)Z_\rho=P_\rho(X_\rho): (i) for V∈{Zρ,Zρ∗}V\in\{Z_\rho,Z_\rho^*\}, χGL(V)≤∥Pρ∥<1+ρ,χDPR(V)=∞; \chi_{\mathrm{GL}}(V)\leq\|P_\rho\|<1+\rho,\qquad\chi_{\mathrm{DPR}}(V)=\infty; (ii) PρP_\rho can be chosen so that ∥I−Pρ∥<1+ρ\|I-P_\rho\|<1+\rho and (i) also holds for (I−Pρ)(Xρ)(I-P_\rho)(X_\rho) and its dual, with PρP_\rho replaced by I−PρI-P_\rho.

The Lean statement requires uniform convexity of the displayed norm, which implies superreflexivity. The manuscript also establishes uniform convexity in Corollary 4.2(ii). The exponents are nonincreasing, and Lean starts the block index at 0.

Exact proposition definition · complete body
def RealMainTheoremStatement : Prop :=
  ∀ ρ : ℝ, 0 < ρ →
    ∃ a : BlockParameters,
      TopologicalSpace.SeparableSpace (Ambient a) ∧
      UniformConvexSpace (Ambient a) ∧
      HasRealBanachLatticeOrder (Ambient a) ∧
      ∃ P : Ambient a →L[ℝ] Ambient a,
        P.comp P = P ∧
        ‖P‖ < 1 + ρ ∧
        ‖ContinuousLinearMap.id ℝ (Ambient a) - P‖ < 1 + ρ ∧
        HasSeparatedRange P ∧
        HasSeparatedRange (ContinuousLinearMap.id ℝ (Ambient a) - P)

Statement source

Proved declaration · proof body omitted
theorem realMainTheorem : RealMainTheoremStatement

Verified in Lean · Source · Verification details

The definition states the result; realMainTheorem proves it.

Theorem B

Mathematical statement · real and complex fields
For K∈{R,C}\mathbb K\in\{\mathbb R,\mathbb C\} and every ρ>0\rho>0, there are a Banach space XρX_\rho over K\mathbb K with a 11-unconditional basis and a projection PρP_\rho on XρX_\rho with ∥Pρ∥<1+ρ\|P_\rho\|<1+\rho such that, writing Zρ=Pρ(Xρ)Z_\rho=P_\rho(X_\rho), neither ZρZ_\rho nor Zρ∗Z_\rho^* admits an unconditional basis. If K=R\mathbb K=\mathbb R, neither space is isomorphic to a Banach lattice.

The real declaration on the right includes the two nonisomorphism conclusions. The common basis conclusion and its complex specialisation follow below.

Real case

Exact proposition definition · complete body
def RealCorollaryStatement : Prop :=
  ∀ ρ : ℝ, 0 < ρ → ∃ X : BanachModel.{0} ℝ,
    HasOneUnconditionalSchauderBasis ℝ X.Carrier ∧
    ∃ P : X.Carrier →L[ℝ] X.Carrier,
      P.comp P = P ∧ ‖P‖ < 1 + ρ ∧
      ¬ HasUnconditionalSchauderBasis ℝ P.range ∧
      ¬ HasUnconditionalSchauderBasis ℝ (P.range →L[ℝ] ℝ) ∧
      ¬ IsIsomorphicToRealBanachLattice P.range ∧
      ¬ IsIsomorphicToRealBanachLattice (P.range →L[ℝ] ℝ)

Statement source

Proved declaration · proof body omitted
theorem realCorollary : RealCorollaryStatement

Verified in Lean · Source · Verification details

Basis conclusion over each field

This proposition states the unconditional-basis part of Theorem B. The theorem realUnconditionalCorollary\mathtt{realUnconditionalCorollary} proves it for R\mathbb R, and complexCorollary\mathtt{complexCorollary} proves its specialisation to C\mathbb C.

The generic proposition is defined for a normed scalar field. The two proved declarations displayed here concern the real and complex fields.

Over ℂ, the operators and continuous dual are complex-linear. The ambient 1-unconditional basis is contractive under complex coordinate multipliers of modulus at most one, including all phases. The complex theorem proves the basis conclusion.

Exact proposition definition · complete body
def UnconditionalCorollaryStatement (𝕜 : Type*) [NontriviallyNormedField 𝕜] : Prop :=
  ∀ ρ : ℝ, 0 < ρ → ∃ X : BanachModel.{0} 𝕜,
    HasOneUnconditionalSchauderBasis 𝕜 X.Carrier ∧
    ∃ P : X.Carrier →L[𝕜] X.Carrier,
      P.comp P = P ∧ ‖P‖ < 1 + ρ ∧
      ¬ HasUnconditionalSchauderBasis 𝕜 P.range ∧
      ¬ HasUnconditionalSchauderBasis 𝕜 (P.range →L[𝕜] 𝕜)

Statement source

Proved declaration · proof body omitted
theorem realUnconditionalCorollary : UnconditionalCorollaryStatement ℝ

Verified in Lean · Source · Verification details

Complex specialisation

Substitute ℂ for the field in the complete proposition just above. This definition adds no new hypotheses or conclusions; the separate theorem below proves that specialisation.

Exact proposition definition · complete body
def ComplexCorollaryStatement : Prop := UnconditionalCorollaryStatement ℂ

Statement source

Proved declaration · proof body omitted
theorem complexCorollary : ComplexCorollaryStatement

Verified in Lean · Source · Verification details

Corollary C

Mathematical statement
The class of separable real Banach lattices is not primary.

The restriction to real scalars and the counterexample are given in §4.3 and Corollary 4.5 of the manuscript.

The counterexample in Lean

For every ρ>0\rho>0 there is a separable real Banach lattice XX, isomorphic to a complete uniformly convex space, with a 11-unconditional Schauder basis and a bounded real-linear map P:X→XP:X\to X such that P2=PP^2=P, ∥P∥<1+ρ\|P\|<1+\rho, ∥I−P∥<1+ρ\|I-P\|<1+\rho, and neither P(X)P(X) nor (I−P)(X)(I-P)(X) is isomorphic to any real Banach lattice.

The Lean statement describes the counterexample: neither complementary summand is isomorphic to a Banach lattice. It does not introduce a general predicate for a primary class. Here superreflexivity means isomorphism to a complete uniformly convex space.

Exact proposition definition · complete body
def SeparableNonprimarityStatement : Prop :=
  ∀ ρ : ℝ, 0 < ρ → ∃ X : BanachModel.{0} ℝ,
    TopologicalSpace.SeparableSpace X.Carrier ∧
    HasRealBanachLatticeOrder X.Carrier ∧
    IsSuperreflexiveByRenorming ℝ X.Carrier ∧
    HasOneUnconditionalSchauderBasis ℝ X.Carrier ∧
    ∃ P : X.Carrier →L[ℝ] X.Carrier,
      P.comp P = P ∧ ‖P‖ < 1 + ρ ∧
      ‖ContinuousLinearMap.id ℝ X.Carrier - P‖ < 1 + ρ ∧
      ¬ IsIsomorphicToRealBanachLattice P.range ∧
      ¬ IsIsomorphicToRealBanachLattice
        (ContinuousLinearMap.id ℝ X.Carrier - P).range

Statement source

Proved declaration · proof body omitted
theorem realSeparableNonprimarity : SeparableNonprimarityStatement

Verified in Lean · Source · Verification details