PL1/Statements.lean

All source files · Download exact source

SHA-256: 6adc0894c6ee4f091160cbc77ffd39afd6afd1b6a6e369e1a0da97653c6dc6b3

1import PL1.Definitions23/-!4# Theorems A and B: full target propositions, awaiting human review56Authoritative source: manuscript/PL1_paper_updated.pdf, page 2, with companion7main.tex labels thm:main and thm:non-schur; scalar convention on pages 2–3.89These declarations DEFINE claims and do not assert proofs of those claims.10For complex scalars the nonlattice clause explicitly targets the stronger11underlying-real obstruction used by the paper's argument. A later formal bridge12to complex Banach-lattice nonisomorphism will be recorded separately; no silent13identification of real and complex lattice predicates is made here.14-/1516noncomputable section17open MeasureTheory18open scoped ENNReal1920namespace PL12122/-- All Theorem A clauses apply to this single projection and its actual range.23Closedness and infinite dimension are explicit consequences of the paper's24projection and failure-of-RNP conclusions. The explicit instance arguments in25the last clauses preserve exactly the inherited range norm when restricting26scalars; they avoid a parent-instance inference ambiguity. -/27def TheoremASpec (𝕜 : Type*) [RCLike 𝕜]28    (P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=29  IsProjection P ∧30  ‖P‖ ≤ projectionBound ∧31  IsClosed (P.range : Set (IntervalL1 𝕜)) ∧32  ¬ FiniteDimensional 𝕜 P.range ∧33  IsDunfordPettis P ∧34  HasSchurProperty 𝕜 P.range ∧35  ¬ @HasRadonNikodymProperty.{_, 0} (UnderlyingReal 𝕜 P.range)36      (inferInstanceAs (NormedAddCommGroup P.range))37      (NormedSpace.restrictScalars ℝ 𝕜 P.range) ∧38  ¬ @HasEquivalentRealLatticeNorm (UnderlyingReal 𝕜 P.range)39      (inferInstanceAs (NormedAddCommGroup P.range))40      (NormedSpace.restrictScalars ℝ 𝕜 P.range)4142/-- Theorem A, with an explicit underlying-real nonlattice conclusion. -/43def TheoremAStatement (𝕜 : Type*) [RCLike 𝕜] : Prop :=44  ∃ P : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜, TheoremASpec 𝕜 P4546/-- All Theorem B clauses apply to this same Q and its inherited range norm. -/47def TheoremBSpec (𝕜 : Type*) [RCLike 𝕜]48    (Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜) : Prop :=49  IsProjection Q ∧50  ‖Q‖ ≤ projectionBound ∧51  IsClosed (Q.range : Set (IntervalL1 𝕜)) ∧52  ¬ FiniteDimensional 𝕜 Q.range ∧53  ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) Q.range ∧54  ¬ ContainsIsomorphicCopy 𝕜 (IntervalL1 𝕜) Q.range ∧55  ¬ HasSchurProperty 𝕜 Q.range ∧56  ¬ @HasEquivalentRealLatticeNorm (UnderlyingReal 𝕜 Q.range)57      (inferInstanceAs (NormedAddCommGroup Q.range))58      (NormedSpace.restrictScalars ℝ 𝕜 Q.range)5960/-- Theorem B, with an explicit underlying-real nonlattice conclusion. -/61def TheoremBStatement (𝕜 : Type*) [RCLike 𝕜] : Prop :=62  ∃ Q : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜, TheoremBSpec 𝕜 Q6364/-- Planned proof declaration: theoremAReal. -/65def TheoremARealStatement : Prop := TheoremAStatement ℝ6667/-- Planned proof declaration: theoremAComplexStrong. The strengthening over68the printed complex theorem is disclosed in this file and the review guide. -/69def TheoremAComplexStrongStatement : Prop := TheoremAStatement ℂ7071/-- Planned proof declaration: theoremBReal. -/72def TheoremBRealStatement : Prop := TheoremBStatement ℝ7374/-- Planned proof declaration: theoremBComplexStrong. -/75def TheoremBComplexStrongStatement : Prop := TheoremBStatement ℂ7677/-- Four separate existences; the real/complex and A/B witnesses may differ. -/78def MainTheoremsStatement : Prop :=79  TheoremARealStatement ∧ TheoremAComplexStrongStatement ∧80  TheoremBRealStatement ∧ TheoremBComplexStrongStatement8182end PL183