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

PL1/ThirdProofReview.lean

All source files · Download exact source

SHA-256: 1f46a6df4070b0d0bacf4e967ced3ce3eb7d86bb38fe4b60513a14796f2e8646

1import PL1.MainTheoremA2import PL1.MainTheoremB3import PL1.EnfloNoL14import PL1.EnfloSmoothing5import PL1.EnfloCopyExclusion6import PL1.ALAlternative7import PL1.FiniteGrothendieck89/-!10# Exact reviewed endpoints and axiom audit for the third pass1112The examples require the original reviewed real and strong complex targets,13without any structural input. The construction uses the original projection14and inherited norm. The arbitrary-L1-copy obstruction is proved directly for15the noise construction; a general Enflo–Starbird extraction theorem is not16asserted. The lattice consequence uses the proved direct AL alternative.17-/1819set_option pp.universes true2021example : PL1.TheoremARealStatement := PL1.theoremAReal22example : PL1.TheoremAComplexStrongStatement := PL1.theoremAComplexStrong23example : PL1.TheoremBRealStatement := PL1.theoremBReal24example : PL1.TheoremBComplexStrongStatement := PL1.theoremBComplexStrong2526example : PL1.MainTheoremsStatement :=27  ⟨PL1.theoremAReal, PL1.theoremAComplexStrong, PL1.theoremBReal, PL1.theoremBComplexStrong⟩2829#print PL1.TheoremBSpec30#print PL1.TheoremBStatement31#print PL1.TheoremBRealStatement32#print PL1.TheoremBComplexStrongStatement33#check @PL1.theoremB34#print axioms PL1.theoremAReal35#print axioms PL1.theoremAComplexStrong36#print axioms PL1.theoremB37#print axioms PL1.theoremBReal38#print axioms PL1.theoremBComplexStrong3940#check @PL1.FiniteSumming.matrixGrothendieckWith_12841#print axioms PL1.FiniteSumming.matrixGrothendieckWith_12842#print axioms PL1.FiniteSumming.oneSumming_12843#print axioms PL1.FiniteSumming.twoSumming_12844#print axioms PL1.DyadicL1Coordinates.analysis_synthesis45#print axioms PL1.DyadicL1Coordinates.norm_synthesis46#check @PL1.IntervalSumming.oneSumming_interval47#check @PL1.IntervalSumming.twoSumming_interval48#print axioms PL1.IntervalSumming.oneSumming_interval49#print axioms PL1.IntervalSumming.twoSumming_interval5051#check @PL1.PositiveLowerOneBridge.positiveLowerOne_of_disjoint52#check @PL1.PositiveLowerOneBridge.positiveLowerOne_of_complemented_ambient53#print axioms PL1.PositiveLowerOneBridge.positiveLowerOne_of_disjoint54#print axioms PL1.PositiveLowerOneBridge.positiveLowerOne_of_complemented_ambient55#print axioms PL1.ALRenorming.seminorm_bounds56#print axioms PL1.ALRenorming.isALNorm57#print axioms PL1.ALAtomic.coordinateIsometry58#print axioms PL1.ALAtomic.hasSchurProperty59#print axioms PL1.ALDyadicEmbedding.containsIsomorphicCopy_of_not_atomic60#check @PL1.ALAlternative.schur_or_contains_interval_of_complemented61#print axioms PL1.ALAlternative.schur_or_contains_interval_of_complemented6263#print axioms PL1.EnfloBush.dyadic_max_integral_mul_norm64#print axioms PL1.EnfloBush.exists_dyadic_majorant65#check @PL1.EnfloBush.noise_comp_dyadicVanishing66#print axioms PL1.EnfloBush.noise_comp_dyadicVanishing67#print axioms PL1.DyadicCoordinateDomination.exists_summable_majorant68#print axioms PL1.EnfloBush.maxMass_flatten69#print axioms PL1.EnfloBush.not_boundedBelow_sum_of_coordinates70#print axioms PL1.EnfloBush.dyadicVanishing_resolvent_of_noise71#print axioms PL1.EnfloBush.dyadicVanishing_intrinsic_evalZero72#print axioms PL1.EnfloBush.dyadicVanishing_intrinsic_flatten73#print axioms PL1.EnfloBush.not_boundedBelow_two_maps74#print axioms PL1.IntrinsicRealParts.norm_le_parts75#print axioms PL1.EnfloBush.scalarIntrinsic_no_real_L1_of_operators76#check @PL1.Noise.constant_intervalProjection_range_no_real_L177#check @PL1.Noise.constant_intervalProjection_range_no_underlying_real_L178#print axioms PL1.Noise.constant_intervalProjection_range_no_real_L179#print axioms PL1.Noise.constant_intervalProjection_range_no_underlying_real_L180