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

PL1/ALAlternative.lean

All source files · Download exact source

SHA-256: 46249b61a963c18dbaf80223354eaa448924a61df8f201e7944fae9252b39a7e

1import PL1.ALAtomic2import PL1.ALDyadicEmbedding3import PL1.PositiveLowerOneBridge4import PL1.IntervalSumming5import PL1.ProjectionTransport67/-!8# The separable complemented-L1 lattice alternative910Actual atomic coordinates give the Schur branch. Actual balanced fragments11give the interval-L1 branch. Finite Grothendieck estimates and the positive12decomposition norm connect this alternative to a complemented Banach lattice13in real interval L1. No representation or extraction theorem is a premise.14-/1516noncomputable section17open TopologicalSpace1819namespace PL1.ALAlternative2021variable {E : Type*} [NormedAddCommGroup E] [Lattice E]22  [IsOrderedAddMonoid E] [NormedVectorLattice E] [CompleteSpace E] [SeparableSpace E]2324/-- Every separable complete AL lattice is Schur or contains actual interval L1. -/25theorem schur_or_contains_interval (hAL : ALRenorming.IsALNorm E) :26    HasSchurProperty ℝ E ∨ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E := by27  by_cases hA : IsAtomicLattice E28  · exact Or.inl (ALAtomic.hasSchurProperty hAL hA)29  · exact Or.inr (ALDyadicEmbedding.containsIsomorphicCopy_of_not_atomic hAL hA)3031/-- A positive finite lower-one bound produces the same alternative in the32original norm, through the actual equivalent AL norm. -/33theorem schur_or_contains_interval_of_positiveLowerOne {C : ℝ}34    (hC : ALRenorming.PositiveLowerOne (E := E) C) :35    HasSchurProperty ℝ E ∨ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E := by36  let : NormedVectorLattice (ALRenorming.Space hC) := ALRenorming.normedVectorLattice hC37  let : CompleteSpace (ALRenorming.Space hC) := ALRenorming.completeSpace hC38  let : SeparableSpace (ALRenorming.Space hC) := ALRenorming.separableSpace hC39  obtain hs | hc := schur_or_contains_interval (ALRenorming.isALNorm hC)40  · exact Or.inl ((hasSchurProperty_equiv_iff (ALRenorming.equiv hC)).mpr hs)41  · exact Or.inr (ContainsIsomorphicCopy.map hc (ALRenorming.equiv hC).symm)4243end PL1.ALAlternative4445namespace PL1.ALAlternative4647variable {E : Type*} [NormedAddCommGroup E] [Lattice E]48  [IsOrderedAddMonoid E] [BanachLattice E] [TopologicalSpace.SeparableSpace E]4950/-- The full direct alternative for an actual complemented real interval-L151Banach lattice. All finite summing and renorming inputs are discharged. -/52theorem schur_or_contains_interval_of_complemented53    (Q : EnfloStarbird.ComplementedCopy ℝ E (IntervalL1 ℝ)) :54    HasSchurProperty ℝ E ∨ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E :=55  schur_or_contains_interval_of_positiveLowerOne56    (PositiveLowerOneBridge.positiveLowerOne_of_complemented_ambient Q57      (by norm_num : (0 : ℝ) ≤ 128) IntervalSumming.oneSumming_interval58      IntervalSumming.twoSumming_interval)5960end PL1.ALAlternative61