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

PL1/ComplementedLatticeReduction.lean

All source files · Download exact source

SHA-256: b396ee685000d31e59dfab0aa1321f411cce999ddcebb6fcf193d4e450904c3e

1import PL1.ComplementedLatticeRealTrace2import PL1.LatticeRenorming34/-! # Explicit structural dependencies for the full reviewed Theorem B56The operator and real trace obstructions used below are proved. The three7structural properties defined in this file are arguments to the endpoint;8they are not asserted as theorems or registered as instances.9-/1011noncomputable section12set_option backward.isDefEq.respectTransparency false13universe u14open MeasureTheory TopologicalSpace Topology1516namespace PL1.ComplementedLattice1718open PL1.EnfloStarbird1920/-- An actual isomorphic real L1 model, including its measure space. -/21def HasRealL1Model (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] : Prop :=22  ∃ (Ω : Type u) (m : MeasurableSpace Ω) (μ : @Measure Ω m),23    Nonempty (E ≃L[ℝ] Lp ℝ 1 μ)2425/-- The complemented-L1 lattice classification, for the actual ambient L126space viewed over the reals. For complex scalars this includes the usual27identification of complex L1, with scalars restricted, with a real L1 space. -/28def ComplementedL1LatticeClassification (K : Type u) [RCLike K] : Prop :=29  ∀ (F : Type u) [NormedAddCommGroup F] [Lattice F] [IsOrderedAddMonoid F]30    [BanachLattice F] [SeparableSpace F],31    Nonempty (ComplementedCopy ℝ F (IntervalL1 K)) → HasRealL1Model F3233/-- The separable L1 classification consequence actually needed here. -/34def SeparableRealL1Dichotomy : Prop :=35  ∀ (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E]36    [CompleteSpace E] [SeparableSpace E], HasRealL1Model E →37      HasSchurProperty ℝ E ∨ ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E3839/-- The real Enflo–Starbird extraction step, restricted to complemented ambient40subspaces as needed by this construction. A proved scalar-to-real copy bridge41below also makes this sufficient to exclude scalar L1 copies. -/42def L1CopyExtraction (K : Type u) [RCLike K] : Prop :=43  ∀ (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E]44    [CompleteSpace E] [SeparableSpace E],45    Nonempty (ComplementedCopy ℝ E (IntervalL1 K)) →46    ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E →47      Nonempty (ComplementedCopy ℝ (IntervalL1 ℝ) E)4849variable {K : Type u} [RCLike K]5051/-- A scalar interval L1 copy contains a real interval L1 copy after restricting52scalars. Closedness and the bounded inverse are preserved explicitly. -/53theorem scalar_L1_copy_contains_real_L1 {E : Type u} [NormedAddCommGroup E]54    [NormedSpace K E] [NormedSpace ℝ E] [IsScalarTower ℝ K E] [CompleteSpace E]55    (h : ContainsIsomorphicCopy K (IntervalL1 K) E) :56    ContainsIsomorphicCopy ℝ (IntervalL1 ℝ) E := by57  obtain ⟨V, hV, ⟨e⟩⟩ := h58  let J : IntervalL1 ℝ →L[ℝ] E := (V.subtypeL.restrictScalars ℝ).comp59    ((e.toContinuousLinearMap.restrictScalars ℝ).comp (intervalOfReal K))60  have ho : IsClosedEmbedding (intervalOfReal K) :=61    (show Function.LeftInverse (intervalRe K) (intervalOfReal K) from intervalRe_ofReal K).isClosedEmbedding62      (intervalRe K).continuous (intervalOfReal K).continuous63  have hJ : IsClosedEmbedding J :=64    (V.isClosedEmbedding_subtypeL hV).comp (e.toHomeomorph.isClosedEmbedding.comp ho)65  exact ⟨J.range, hJ.isClosed_range, ⟨J.equivRange hJ.injective hJ.isClosed_range⟩⟩6667/-- Identity on vectors, with the natural compatible real action on the source68and the explicitly restricted action used in the reviewed target on the target. -/69def naturalToUnderlyingReal (E : Type u) [NormedAddCommGroup E] [NormedSpace K E]70    [NormedSpace ℝ E] [IsScalarTower ℝ K E] : E ≃L[ℝ] UnderlyingReal K E where71  toFun := fun x => x72  invFun := fun x => x73  left_inv := fun _ => rfl74  right_inv := fun _ => rfl75  map_add' := fun _ _ => rfl76  map_smul' := fun c x => by77    change c • x = algebraMap ℝ K c • x78    exact (IsScalarTower.algebraMap_smul K c x).symm79  continuous_toFun := continuous_id80  continuous_invFun := continuous_id8182def projectionRangeCopy (Q : IntervalL1 K →L[K] IntervalL1 K) (hQ : IsProjection Q) :83    ComplementedCopy K Q.range (IntervalL1 K) where84  embedding := Q.range.subtypeL85  retraction := Q.rangeRestrict86  left_inv := fun x => Subtype.ext (hQ.apply_range x)8788def projectionRangeCopyReal (Q : IntervalL1 K →L[K] IntervalL1 K) (hQ : IsProjection Q) :89    ComplementedCopy ℝ Q.range (IntervalL1 K) := by90  exact ⟨Q.range.subtypeL.restrictScalars ℝ, Q.rangeRestrict.restrictScalars ℝ,91    fun x => Subtype.ext (hQ.apply_range x)⟩9293def complementedCopyTransport {E : Type*} {F : Type*} {G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]94    [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G]95    (C : ComplementedCopy ℝ E G) (e : E ≃L[ℝ] F) : ComplementedCopy ℝ F G where96  embedding := C.embedding.comp e.symm.toContinuousLinearMap97  retraction := e.toContinuousLinearMap.comp C.retraction98  left_inv := fun x => (congrArg e (C.left_inv (e.symm x))).trans (e.apply_symm_apply x)99100/-- The actual scalar projection range contains no complemented scalar interval L1. -/101theorem constant_range_no_complemented_scalar_L1 :102    ¬ Nonempty (ComplementedCopy K (IntervalL1 K)103      (Noise.intervalProjection K Noise.constantRates).range) := by104  rw [← identityFactorsThrough_iff_complementedCopy_range _105    (Noise.intervalProjection_isProjection K Noise.constantRates)]106  rintro ⟨A, B, h⟩107  exact Noise.constant_intervalProjection_not_factors_identity K A B h108109/-- The stronger real obstruction follows from real vanishing trace, including110when the projection and its range were originally constructed over ℂ. -/111theorem constant_range_no_complemented_real_L1 :112    ¬ Nonempty (ComplementedCopy ℝ (IntervalL1 ℝ)113      (Noise.intervalProjection K Noise.constantRates).range) := by114  let Q := Noise.intervalProjection K Noise.constantRates115  rintro ⟨C⟩116  let A := C.retraction.comp (Q.rangeRestrict.restrictScalars ℝ)117  let B := (Q.range.subtypeL.restrictScalars ℝ).comp C.embedding118  apply (constant_intervalProjection_real_hasVanishingDyadicTrace K).not_factors_identity A B119  ext1 f120  change C.retraction ⟨Q (Q (C.embedding f)), _⟩ = f121  have hq := Noise.intervalProjection_isProjection K Noise.constantRates122  have hx : (⟨Q (Q (C.embedding f)), by exact ⟨Q (C.embedding f), rfl⟩⟩ : Q.range) =123      C.embedding f := by124    apply Subtype.ext125    exact (DFunLike.congr_fun hq (C.embedding f : IntervalL1 K)).trans126      (hq.apply_range (C.embedding f))127  rw [hx]128  exact C.left_inv f129130/-- Precisely the reviewed full B target, conditional on the displayed131classification, dichotomy, and arbitrary-copy extraction properties. -/132theorem theoremB_of_structural_properties (K : Type u) [RCLike K]133    (hclass : ComplementedL1LatticeClassification K)134    (hdich : SeparableRealL1Dichotomy.{u}) (hextract : L1CopyExtraction K) :135    TheoremBStatement K := by136  let Q := Noise.intervalProjection K Noise.constantRates137  have hQ := Noise.intervalProjection_isProjection K Noise.constantRates138  have hclosed := Noise.intervalProjection_range_isClosed K Noise.constantRates139  let : CompleteSpace Q.range := hclosed.isComplete.completeSpace_coe140  let : SeparableSpace (Noise.projection K Noise.constantRates).range :=141    Noise.projection_range_separableSpace K Noise.constantRates142  let e := Noise.intervalProjectionRangeEquiv K Noise.constantRates143  let : SeparableSpace Q.range := e.surjective.denseRange.separableSpace e.continuous144  let : CompleteSpace (UnderlyingReal K Q.range) := inferInstanceAs (CompleteSpace Q.range)145  let : SeparableSpace (UnderlyingReal K Q.range) := inferInstanceAs (SeparableSpace Q.range)146  refine ⟨Q, hQ, Noise.norm_intervalProjection_le K Noise.constantRates, hclosed,147    Noise.intervalProjection_range_infiniteDimensional K Noise.constantRates,148    Noise.constant_intervalProjection_range_contains_ell2 K, ?_,149    Noise.constant_intervalProjection_range_not_schur K, ?_⟩150  · intro hcopy151    exact constant_range_no_complemented_real_L1152      (hextract Q.range ⟨projectionRangeCopyReal Q hQ⟩153        (scalar_L1_copy_contains_real_L1 hcopy))154  ·155    intro hlat156    apply hlat.elim_separable157    intro F _ _ _ _ _ eF158    let eFn : Q.range ≃L[ℝ] F := (naturalToUnderlyingReal (K := K) Q.range).trans eF159    have hCF : Nonempty (ComplementedCopy ℝ F (IntervalL1 K)) :=160      ⟨complementedCopyTransport (projectionRangeCopyReal Q hQ) eFn⟩161    obtain hs | hc := hdich F (hclass F hCF)162    · exact Noise.constant_intervalProjection_range_not_schur K163        ((hasSchurProperty_iff_real (𝕜 := K) (E := Q.range)).mpr164          ((hasSchurProperty_equiv_iff eFn).mpr hs))165    · have hcQ := hc.map eFn.symm166      exact constant_range_no_complemented_real_L1167        (hextract Q.range ⟨projectionRangeCopyReal Q hQ⟩ hcQ)168169#print axioms constant_range_no_complemented_real_L1170#print axioms theoremB_of_structural_properties171172end PL1.ComplementedLattice173