PL1/PartialMainTheorems.lean

All source files · Download exact source

SHA-256: 0a49a12ca6b52034ec888a4e13a6ae75fb6ef3cbf8d10a885b8776c8a19e3d87

1import PL1.Statements2import PL1.IntervalWalsh3import PL1.SchurExample4import PL1.SingularResolvents5import PL1.RNPTransport6import PL1.RealSchur7import PL1.SeparableRange89/-!10# Proved interval-level parts of the main theorems1112These are concrete existence results on the reviewed interval L1 space.13Theorem A's nonlattice clause and Theorem B's exclusion of L1 copies and14nonlattice clause are not asserted here. The full reviewed target definitions15in `PL1.Statements` remain unchanged. `PL1.MainTheoremA` now proves all of A;16the complete B endpoint remains conditional on explicit structural results.17-/1819noncomputable section20open MeasureTheory21open scoped ENNReal NNReal2223namespace PL1.Noise2425variable (𝕜 : Type*) [RCLike 𝕜]2627/-- The actual projection on L1([0,1]), obtained through the constructed28isometric embedding and contractive retraction. -/29def intervalProjection (rates : ℕ → ℝ≥0) : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜 :=30  (IntervalWalsh.walshSumContractiveRetract 𝕜).transport (projection 𝕜 rates)3132def intervalProjectionRangeEquiv (rates : ℕ → ℝ≥0) :33    (projection 𝕜 rates).range ≃L[𝕜] (intervalProjection 𝕜 rates).range :=34  (IntervalWalsh.walshSumContractiveRetract 𝕜).rangeEquiv (projection 𝕜 rates)3536theorem intervalProjection_isProjection (rates : ℕ → ℝ≥0) :37    IsProjection (intervalProjection 𝕜 rates) :=38  (IntervalWalsh.walshSumContractiveRetract 𝕜).isProjection (projection_isProjection 𝕜 rates)3940theorem norm_intervalProjection_le (rates : ℕ → ℝ≥0) :41    ‖intervalProjection 𝕜 rates‖ ≤ projectionBound :=42  ((IntervalWalsh.walshSumContractiveRetract 𝕜).norm_transport_le _).trans43    (norm_projection_le 𝕜 rates)4445theorem intervalProjection_range_isClosed (rates : ℕ → ℝ≥0) :46    IsClosed ((intervalProjection 𝕜 rates).range : Set (IntervalL1 𝕜)) :=47  (intervalProjection_isProjection 𝕜 rates).isClosed_range4849theorem intervalProjection_range_infiniteDimensional (rates : ℕ → ℝ≥0) :50    ¬ FiniteDimensional 𝕜 (intervalProjection 𝕜 rates).range := by51  intro h52  exact projection_range_infiniteDimensional 𝕜 rates53    (((IntervalWalsh.walshSumContractiveRetract 𝕜).finiteDimensional_range_iff _).mp h)5455theorem schur_intervalProjection_isDunfordPettis :56    IsDunfordPettis (intervalProjection 𝕜 schurRates) :=57  (IntervalWalsh.walshSumContractiveRetract 𝕜).isDunfordPettis58    (schurRates_projection_isDunfordPettis 𝕜)5960theorem schur_intervalProjection_range_hasSchurProperty :61    HasSchurProperty 𝕜 (intervalProjection 𝕜 schurRates).range :=62  (hasSchurProperty_equiv_iff (intervalProjectionRangeEquiv 𝕜 schurRates)).mp63    (schurRates_projection_range_hasSchurProperty 𝕜)6465theorem schur_intervalProjection_range_not_RNP :66    ¬ @HasRadonNikodymProperty.{_, 0}67      (UnderlyingReal 𝕜 (intervalProjection 𝕜 schurRates).range)68      (inferInstanceAs (NormedAddCommGroup (intervalProjection 𝕜 schurRates).range))69      (NormedSpace.restrictScalars ℝ 𝕜 (intervalProjection 𝕜 schurRates).range) := by70  intro h71  exact schur_projection_range_not_RNP 𝕜72    ((RNPTransport.hasRadonNikodymProperty_restrictScalars_iff73      (intervalProjectionRangeEquiv 𝕜 schurRates)).mpr h)7475theorem constant_intervalProjection_range_contains_ell2 :76    ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) (intervalProjection 𝕜 constantRates).range :=77  (constantRates_projection_range_contains_ell2 𝕜).map78    (intervalProjectionRangeEquiv 𝕜 constantRates)7980theorem constant_intervalProjection_range_not_schur :81    ¬ HasSchurProperty 𝕜 (intervalProjection 𝕜 constantRates).range :=82  not_hasSchurProperty_of_contains_ell2 𝕜83    (constant_intervalProjection_range_contains_ell2 𝕜)8485theorem constant_intervalProjection_range_not_RNP :86    ¬ @HasRadonNikodymProperty.{_, 0}87      (UnderlyingReal 𝕜 (intervalProjection 𝕜 constantRates).range)88      (inferInstanceAs (NormedAddCommGroup (intervalProjection 𝕜 constantRates).range))89      (NormedSpace.restrictScalars ℝ 𝕜 (intervalProjection 𝕜 constantRates).range) := by90  intro h91  exact constant_projection_range_not_RNP 𝕜92    ((RNPTransport.hasRadonNikodymProperty_restrictScalars_iff93      (intervalProjectionRangeEquiv 𝕜 constantRates)).mpr h)9495end PL1.Noise9697namespace PL19899/-- All reviewed Theorem A clauses except nonlattice, for one actual interval100projection. `PL1.MainTheoremA` supplies the full theorem separately. -/101theorem theoremA_except_nonlattice (𝕜 : Type*) [RCLike 𝕜] :102    ∃ P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜,103      IsProjection P ∧ ‖P‖ ≤ projectionBound ∧104      IsClosed (P.range : Set (IntervalL1 𝕜)) ∧ ¬ FiniteDimensional 𝕜 P.range ∧105      IsDunfordPettis P ∧ HasSchurProperty 𝕜 P.range ∧106      ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 P.range)107        (inferInstanceAs (NormedAddCommGroup P.range))108        (NormedSpace.restrictScalars ℝ 𝕜 P.range) :=109  ⟨Noise.intervalProjection 𝕜 Noise.schurRates,110    Noise.intervalProjection_isProjection 𝕜 Noise.schurRates,111    Noise.norm_intervalProjection_le 𝕜 Noise.schurRates,112    Noise.intervalProjection_range_isClosed 𝕜 Noise.schurRates,113    Noise.intervalProjection_range_infiniteDimensional 𝕜 Noise.schurRates,114    Noise.schur_intervalProjection_isDunfordPettis 𝕜,115    Noise.schur_intervalProjection_range_hasSchurProperty 𝕜,116    Noise.schur_intervalProjection_range_not_RNP 𝕜⟩117118/-- The constructed non-Schur interval projection and its closed ell2 copy.119The exclusion of L1 copies and the nonlattice clause are still unproved.120The additional RNP failure is the paper's later non-Schur geometry claim. -/121theorem theoremB_partial (𝕜 : Type*) [RCLike 𝕜] :122    ∃ Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜,123      IsProjection Q ∧ ‖Q‖ ≤ projectionBound ∧124      IsClosed (Q.range : Set (IntervalL1 𝕜)) ∧ ¬ FiniteDimensional 𝕜 Q.range ∧125      ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) Q.range ∧ ¬ HasSchurProperty 𝕜 Q.range ∧126      ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 Q.range)127        (inferInstanceAs (NormedAddCommGroup Q.range))128        (NormedSpace.restrictScalars ℝ 𝕜 Q.range) :=129  ⟨Noise.intervalProjection 𝕜 Noise.constantRates,130    Noise.intervalProjection_isProjection 𝕜 Noise.constantRates,131    Noise.norm_intervalProjection_le 𝕜 Noise.constantRates,132    Noise.intervalProjection_range_isClosed 𝕜 Noise.constantRates,133    Noise.intervalProjection_range_infiniteDimensional 𝕜 Noise.constantRates,134    Noise.constant_intervalProjection_range_contains_ell2 𝕜,135    Noise.constant_intervalProjection_range_not_schur 𝕜,136    Noise.constant_intervalProjection_range_not_RNP 𝕜⟩137138end PL1139