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

PL1/Review.lean

All source files · Download exact source

SHA-256: f9b8488578c267a9cea523cb4c1bd626e1227b0b0d59e670667cc67a06ec623a

1import PL123/-!4Human-review entry point. The four main claims below are propositions, not5proved theorems. The two BanLat bridges at the end are proved theorems.6Run this file to obtain expanded definitions and their actual axiom lists.7-/89noncomputable section1011set_option pp.universes true12set_option pp.fullNames true13set_option pp.proofs false1415#print PL1.intervalMeasure16#print PL1.IntervalL117#print PL1.Ell218#print PL1.Ell119#print PL1.UnderlyingReal20#print PL1.underlyingRealNormedSpace21#print PL1.projectionBound22#print PL1.WeaklyConverges23#print PL1.HasSchurProperty24#print PL1.IsDunfordPettis25#print PL1.IsProjection26#print PL1.ContainsIsomorphicCopy27#print PL1.HasRadonNikodymProperty28#print PL1.HasEquivalentRealLatticeNorm29#print PL1.TheoremASpec30#print PL1.TheoremBSpec31#print PL1.TheoremAStatement32#print PL1.TheoremBStatement33#print PL1.TheoremARealStatement34#print PL1.TheoremAComplexStrongStatement35#print PL1.TheoremBRealStatement36#print PL1.TheoremBComplexStrongStatement37#print PL1.MainTheoremsStatement3839-- These ask Lean for actual standard-space instances, without assuming them.40example : NormedSpace ℝ (PL1.IntervalL1 ℝ) := inferInstance41example : NormedSpace ℂ (PL1.IntervalL1 ℂ) := inferInstance42example : CompleteSpace (PL1.IntervalL1 ℝ) := inferInstance43example : CompleteSpace (PL1.IntervalL1 ℂ) := inferInstance44example : CompleteSpace (PL1.Ell2 ℝ) := inferInstance45example : CompleteSpace (PL1.Ell2 ℂ) := inferInstance46example : NormedSpace ℝ (PL1.UnderlyingReal ℂ (PL1.IntervalL1 ℂ)) := inferInstance4748-- The norm of the underlying real type is definitionally the original norm.49example (x : PL1.IntervalL1 ℂ) :50    ‖(show PL1.UnderlyingReal ℂ (PL1.IntervalL1 ℂ) from x)‖ = ‖x‖ := rfl5152#check PL1.hasEquivalentRealLatticeNorm_of_continuousLinearEquiv53#check PL1.not_nonempty_continuousLinearEquiv_of_not_hasEquivalentRealLatticeNorm54#print axioms PL1.hasEquivalentRealLatticeNorm_of_continuousLinearEquiv55#print axioms PL1.not_nonempty_continuousLinearEquiv_of_not_hasEquivalentRealLatticeNorm5657-- This audits definitions only: it does not turn the four targets into proofs.58#print axioms PL1.MainTheoremsStatement59