PL1/IntervalEll1Obstruction.lean

All source files · Download exact source

SHA-256: 7119cc5de0cb64013afcac5fa014cec206cf95220c2e0fffebdc471c7ddf56bc

1import PL1.PartialMainTheorems2import PL1.Ell1RNP34/-! # Neither actual interval projection range is isomorphic to scalar ell156These consequences of full RNP failure do not assert absence of an interval7L1 subspace and do not complete the nonlattice obstruction.8-/910noncomputable section11namespace PL1.Noise1213theorem schur_intervalProjection_range_not_isomorphic_ell1 (𝕜 : Type*) [RCLike 𝕜] :14    IsEmpty ((intervalProjection 𝕜 schurRates).range ≃L[𝕜] Ell1 𝕜) :=15  Ell1RNP.not_isomorphic_of_not_RNP 𝕜 (schur_intervalProjection_range_not_RNP 𝕜)1617theorem constant_intervalProjection_range_not_isomorphic_ell1 (𝕜 : Type*) [RCLike 𝕜] :18    IsEmpty ((intervalProjection 𝕜 constantRates).range ≃L[𝕜] Ell1 𝕜) :=19  Ell1RNP.not_isomorphic_of_not_RNP 𝕜 (constant_intervalProjection_range_not_RNP 𝕜)2021end PL1.Noise22