On complemented subspaces of L1[0,1]L_1[0,1]

On complemented subspaces of L1[0,1]L_1[0,1]

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 ATheorem B

Theorem A

The Schur example
Mathematical statement Paper, p. 2

There is a Dunford–Pettis projection PP on L1[0,1]L_1[0,1] such that

∥P∥≤4+32.\lVert P\rVert\leq 4+3\sqrt{2}.

Its range has the Schur property but fails the Radon–Nikodým property. In particular, it is not isomorphic to any Banach lattice.

The paper works over K∈{R,C}\mathbb K\in\{\mathbb R,\mathbb C\}. The Lean formulation also makes closedness and infinite dimension explicit. In the complex case, its nonlattice conclusion excludes every equivalent real lattice norm on the underlying real range. The general bridge to complex Banach-lattice nonisomorphism is not separately formalised; see verification scope.

Exact Lean proposition
PL1/Statements.lean:27
def TheoremASpec (𝕜 : Type*) [RCLike 𝕜]
    (P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=
  IsProjection P ∧
  ‖P‖ ≤ projectionBound ∧
  IsClosed (P.range : Set (IntervalL1 𝕜)) ∧
  ¬ FiniteDimensional 𝕜 P.range ∧
  IsDunfordPettis P ∧
  HasSchurProperty 𝕜 P.range ∧
  ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 P.range)
      (inferInstanceAs (NormedAddCommGroup P.range))
      (NormedSpace.restrictScalars ℝ 𝕜 P.range) ∧
  ¬ @HasEquivalentRealLatticeNorm (UnderlyingReal 𝕜 P.range)
      (inferInstanceAs (NormedAddCommGroup P.range))
      (NormedSpace.restrictScalars ℝ 𝕜 P.range)
PL1/Statements.lean:43
def TheoremAStatement (𝕜 : Type*) [RCLike 𝕜] : Prop :=
  ∃ P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜, TheoremASpec 𝕜 P
PL1/Statements.lean:65
def TheoremARealStatement : Prop := TheoremAStatement ℝ
PL1/Statements.lean:69
def TheoremAComplexStrongStatement : Prop := TheoremAStatement ℂ

def … : Prop names a claim. The separate proved declarations are PL1.theoremA, PL1.theoremAReal and PL1.theoremAComplexStrong. Their proof bodies are in the linked source. README: the formal proof routes.

Read the Lean statement step by step

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def TheoremASpec (𝕜 : Type*) [RCLike 𝕜]
    (P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=
  IsProjection P ∧
  ‖P‖ ≤ projectionBound ∧
  IsClosed (P.range : Set (IntervalL1 𝕜)) ∧
  ¬ FiniteDimensional 𝕜 P.range ∧
  IsDunfordPettis P ∧
  HasSchurProperty 𝕜 P.range ∧
  ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 P.range)
      (inferInstanceAs (NormedAddCommGroup P.range))
      (NormedSpace.restrictScalars ℝ 𝕜 P.range) ∧
  ¬ @HasEquivalentRealLatticeNorm (UnderlyingReal 𝕜 P.range)
      (inferInstanceAs (NormedAddCommGroup P.range))
      (NormedSpace.restrictScalars ℝ 𝕜 P.range)

def TheoremAStatement (𝕜 : Type*) [RCLike 𝕜] : Prop :=
  ∃ P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜, TheoremASpec 𝕜 P

def TheoremARealStatement : Prop := TheoremAStatement ℝ

def TheoremAComplexStrongStatement : Prop := TheoremAStatement ℂ
1 / 12

The conditions on one projection P

def TheoremASpec (𝕜 : Type*) [RCLike 𝕜]
    (P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=
How to read it
def … : Prop := defines a proposition. (𝕜 : Type*) [RCLike 𝕜] fixes a scalar type with Mathlib’s real/complex structure. P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜 fixes a bounded scalar-linear operator.
Mathematical meaning
The conditions below concern this one operator on the actual interval L1L_1 space. The real and complex choices are stated separately at the end.
Role in the statement
This definition lists the conditions; the later existence proposition chooses the operator. A definition alone is not a proof.
IntervalL1Complete source and context

Theorem B

The non-Schur example
Mathematical statement Paper, p. 2

There is a projection QQ on L1[0,1]L_1[0,1], with ∥Q∥≤4+32\lVert Q\rVert\leq4+3\sqrt{2}, whose range contains an isomorphic copy of ℓ2\ell_2 but no isomorphic copy of L1[0,1]L_1[0,1].

In particular, its range does not have the Schur property and is not isomorphic to any Banach lattice.

The paper works over K∈{R,C}\mathbb K\in\{\mathbb R,\mathbb C\}. The Lean formulation also makes closedness and infinite dimension explicit. In the complex case, its nonlattice conclusion excludes every equivalent real lattice norm on the underlying real range. The general bridge to complex Banach-lattice nonisomorphism is not separately formalised; see verification scope.

Exact Lean proposition
PL1/Statements.lean:47
def TheoremBSpec (𝕜 : Type*) [RCLike 𝕜]
    (Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=
  IsProjection Q ∧
  ‖Q‖ ≤ projectionBound ∧
  IsClosed (Q.range : Set (IntervalL1 𝕜)) ∧
  ¬ FiniteDimensional 𝕜 Q.range ∧
  ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) Q.range ∧
  ¬ ContainsIsomorphicCopy 𝕜 (IntervalL1 𝕜) Q.range ∧
  ¬ HasSchurProperty 𝕜 Q.range ∧
  ¬ @HasEquivalentRealLatticeNorm (UnderlyingReal 𝕜 Q.range)
      (inferInstanceAs (NormedAddCommGroup Q.range))
      (NormedSpace.restrictScalars ℝ 𝕜 Q.range)
PL1/Statements.lean:61
def TheoremBStatement (𝕜 : Type*) [RCLike 𝕜] : Prop :=
  ∃ Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜, TheoremBSpec 𝕜 Q
PL1/Statements.lean:72
def TheoremBRealStatement : Prop := TheoremBStatement ℝ
PL1/Statements.lean:75
def TheoremBComplexStrongStatement : Prop := TheoremBStatement ℂ

def … : Prop names a claim. The separate proved declarations are PL1.theoremB, PL1.theoremBReal and PL1.theoremBComplexStrong. Their proof bodies are in the linked source. README: the formal proof routes.

Read the Lean statement step by step

Select a clause in the Lean code, or use Previous and Next. Links within a clause open its definition.

def TheoremBSpec (𝕜 : Type*) [RCLike 𝕜]
    (Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=
  IsProjection Q ∧
  ‖Q‖ ≤ projectionBound ∧
  IsClosed (Q.range : Set (IntervalL1 𝕜)) ∧
  ¬ FiniteDimensional 𝕜 Q.range ∧
  ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) Q.range ∧
  ¬ ContainsIsomorphicCopy 𝕜 (IntervalL1 𝕜) Q.range ∧
  ¬ HasSchurProperty 𝕜 Q.range ∧
  ¬ @HasEquivalentRealLatticeNorm (UnderlyingReal 𝕜 Q.range)
      (inferInstanceAs (NormedAddCommGroup Q.range))
      (NormedSpace.restrictScalars ℝ 𝕜 Q.range)

def TheoremBStatement (𝕜 : Type*) [RCLike 𝕜] : Prop :=
  ∃ Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜, TheoremBSpec 𝕜 Q

def TheoremBRealStatement : Prop := TheoremBStatement ℝ

def TheoremBComplexStrongStatement : Prop := TheoremBStatement ℂ
1 / 12

The conditions on one projection Q

def TheoremBSpec (𝕜 : Type*) [RCLike 𝕜]
    (Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=
How to read it
def … : Prop := defines a proposition. (𝕜 : Type*) [RCLike 𝕜] fixes a scalar type with Mathlib’s real/complex structure. Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜 fixes a bounded scalar-linear operator.
Mathematical meaning
The conditions below concern this one operator on the actual interval L1L_1 space. The real and complex choices are stated separately at the end.
Role in the statement
This definition lists the conditions; the later existence proposition chooses the operator. A definition alone is not a proof.
IntervalL1Complete source and context