PL1/MainTheoremA.lean

All source files · Download exact source

SHA-256: 0203389e42ab458319cc1bf912db8482792417c132484e2934871135daf57b3a

1import PL1.LatticeReduction2import PL1.SchurLatticeAtomicity34/-!5# The full reviewed Theorem A67The actual Schur counterexample admits no equivalent real Banach-lattice8structure: separable Schur Banach lattices have the full vector-measure RNP,9whereas this complemented range does not. The complex endpoint retains the10reviewed, stronger prohibition on its underlying real space.11-/1213noncomputable section14universe u1516namespace PL11718theorem separableSchurLatticeRNP : SeparableSchurLatticeRNP.{u} := by19  intro F _ _ _ _ _ hS20  exact SchurLattice.hasRadonNikodymProperty_of_schur hS2122theorem theoremA (𝕜 : Type u) [RCLike 𝕜] : TheoremAStatement 𝕜 :=23  theoremA_of_separableSchurLatticeRNP 𝕜 separableSchurLatticeRNP2425theorem theoremAReal : TheoremARealStatement := theoremA ℝ2627theorem theoremAComplexStrong : TheoremAComplexStrongStatement := theoremA ℂ2829end PL130