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

PL1/ProofReview.lean

All source files · Download exact source

SHA-256: 1f0f962c528b5550a2a3d23cc09018bb94b016ae073852d286e24f714b792f7f

1import PL1.PartialMainTheorems2import PL1.DyadicTrace3import PL1.FiniteDimensionalRNP4import PL1.MetricApproximation5import PL1.IntrinsicNonBoundedComplete6import PL1.BochnerResolvents7import PL1.SchurLattice8import PL1.LatticeDisjointCountability9import PL1.OperatorDomination10import PL1.LpOperatorLift11import PL1.HilbertTraceBounds12import PL1.SmoothingApproximation13import PL1.IntervalEll1Obstruction14import PL1.ScalarUnconditionalRNP15import PL1.MatrixSmoothing16import PL1.LatticeReduction1718/-! # Exact result and axiom inspection for the three-hour construction1920This review retains the first pass's partial endpoints, with concrete interval21witnesses and no assumed analytic construction hypotheses. The full A proof22and subsequent results are inspected in `PL1.SecondProofReview`; full B remains23conditional on explicit structural results.24-/2526set_option pp.universes true2728#check @PL1.theoremA_except_nonlattice29#check @PL1.theoremB_partial30#check PL1.theoremA_except_nonlattice ℝ31#check PL1.theoremA_except_nonlattice ℂ32#check PL1.theoremB_partial ℝ33#check PL1.theoremB_partial ℂ3435#print axioms PL1.theoremA_except_nonlattice36#print axioms PL1.theoremB_partial37#print axioms PL1.Noise.schurRates_projection_range_underlyingReal_hasSchurProperty38#print axioms PL1.Noise.projection_range_underlyingReal_separableSpace39#print axioms PL1.RNPBridge.hasRadonNikodymProperty_of_finiteDimensional40#print axioms PL1.RNPTransport.hasRadonNikodymProperty_restrictScalars_iff41#print axioms PL1.ContractiveRetract.norm_transport_le42#print axioms PL1.ContractiveRetract.rangeEquiv_norm4344#check @PL1.DyadicTrace.trace45#check @PL1.DyadicTrace.norm_trace_le46#check @PL1.DyadicTrace.trace_id47#check @PL1.DyadicTrace.one_le_norm_id_sub48#print axioms PL1.DyadicTrace.norm_trace_le49#print axioms PL1.DyadicTrace.trace_id50#print axioms PL1.DyadicTrace.one_le_norm_id_sub5152#check @PL1.Noise.intrinsic_hasMetricApproximationProperty53#check @PL1.Noise.finrank_intrinsicExpectation54#check @PL1.Noise.finrank_intrinsicBlock55#check @PL1.Noise.intrinsicBlock_expansion_unique56#check @PL1.Noise.schur_intrinsic_exists_nonCauchy_branch57#check @PL1.Noise.constant_intrinsic_exists_nonCauchy_branch58#check PL1.Noise.schur_intrinsic_exists_nonCauchy_branch ℂ59#check PL1.Noise.constant_intrinsic_exists_nonCauchy_branch ℂ60#check @PL1.ScalarDecompositionRNP.hasRNP_of_scalar_projections61#check @PL1.UnconditionalRNP.hasRadonNikodymProperty_of_schur_unconditional_projections62#check @PL1.Noise.resolventL1_eq_integral63#check @PL1.Noise.norm_resolventL1_sub_truncated_le6465#print axioms PL1.Noise.intrinsic_hasMetricApproximationProperty66#print axioms PL1.Noise.norm_intrinsicExpectation_eq_one67#print axioms PL1.Noise.finrank_intrinsicExpectation68#print axioms PL1.Noise.finrank_intrinsicBlock69#print axioms PL1.Noise.intrinsicBlock_comp70#print axioms PL1.Noise.intrinsicBlock_expansion_unique71#print axioms PL1.Noise.tendsto_intrinsicBlock_partialSum72#print axioms PL1.Noise.schur_intrinsic_not_boundedlyComplete73#print axioms PL1.Noise.constant_intrinsic_not_boundedlyComplete74#print axioms PL1.Noise.schur_intrinsic_exists_nonCauchy_branch75#print axioms PL1.Noise.constant_intrinsic_exists_nonCauchy_branch76#print axioms PL1.Noise.schur_intrinsic_no_uniform_sign_bound77#print axioms PL1.DecompositionRNP.hasRadonNikodymProperty_of_boundedlyCompleteDecomposition78#print axioms PL1.ScalarDecompositionRNP.hasRNP_of_scalar_projections79#print axioms PL1.UnconditionalRNP.hasRadonNikodymProperty_of_schur_unconditional_projections80#print axioms PL1.Noise.noiseL1_add81#print axioms PL1.Noise.continuous_noiseL1_apply82#print axioms PL1.Noise.resolventL1_strong_zero83#print axioms PL1.Noise.resolventL1_eq_integral84#print axioms PL1.Noise.norm_resolventL1_sub_truncated_le85#print axioms PL1.Noise.truncatedResolventL1_tendsto86#print axioms PL1.SchurLattice.tendsto_zero_of_antitone_net_isGLB87#print axioms PL1.SchurLattice.conditionallyCompleteLattice88#print axioms PL1.SchurLattice.exists_countable_maximal_disjoint_positive_family89#print axioms PL1.OperatorDomination.exists_measurable_dominator90#print axioms PL1.OperatorDomination.cutoff_approximation91#print axioms PL1.OperatorDomination.maskedRestrictionLp92#print axioms PL1.LpInterpolation.norm_toLp_le_of_ae_norm_bound93#print axioms PL1.HilbertTraceBounds.sum_cell_dual_norm_sq_le94#print axioms PL1.HilbertTraceBounds.norm_sum_cell_apply_le9596#check @PL1.SmoothingTrace.trace_tendsto_zero_of_smoothing97#check @PL1.SmoothingTrace.one_le_norm_id_sub_of_smoothing98#check @PL1.SmoothingTrace.trace_tendsto_zero_of_smoothing_approximation99#check @PL1.SmoothingTrace.one_le_norm_id_sub_of_smoothing_approximation100#print axioms PL1.SmoothingTrace.trace_tendsto_zero_of_smoothing101#print axioms PL1.SmoothingTrace.one_le_norm_id_sub_of_smoothing102#print axioms PL1.SmoothingTrace.trace_tendsto_zero_of_smoothing_approximation103#print axioms PL1.SmoothingTrace.one_le_norm_id_sub_of_smoothing_approximation104105#check @PL1.Ell1RNP.hasRadonNikodymProperty106#check PL1.Noise.schur_intervalProjection_range_not_isomorphic_ell1 ℂ107#check PL1.Noise.constant_intervalProjection_range_not_isomorphic_ell1 ℂ108#print axioms PL1.Ell1RNP.hasRadonNikodymProperty109#print axioms PL1.Noise.schur_intervalProjection_range_not_isomorphic_ell1110#print axioms PL1.Noise.constant_intervalProjection_range_not_isomorphic_ell1111112#check PL1.Noise.schur_intrinsic_no_uniform_scalar_sign_bound ℂ113#print axioms PL1.Noise.schur_intrinsic_no_uniform_scalar_sign_bound114115#check @PL1.InputCompression.norm_input_compression_error_tendsto_zero116#check @PL1.OutputCompression.tendsto_output_compression117#check @PL1.MatrixTrace.trace_tendsto_zero_of_smoothing_entries118#check @PL1.MatrixTrace.one_le_norm_id_sub_of_smoothing_entries119#print axioms PL1.InputCompression.norm_input_compression_error_tendsto_zero120#print axioms PL1.OutputCompression.tendsto_output_compression121#print axioms PL1.MatrixTrace.trace_tendsto_zero_of_smoothing_entries122#print axioms PL1.MatrixTrace.one_le_norm_id_sub_of_smoothing_entries123124#check @PL1.hasEquivalentRealLatticeNorm_iff_hasBanachLatticeModel125#print axioms PL1.hasEquivalentRealLatticeNorm_iff_hasBanachLatticeModel126127-- This reduction remains conditional in its type. `PL1.MainTheoremA` now128-- discharges the premise; an axiom list alone does not discharge a parameter.129#print PL1.SeparableSchurLatticeRNP130#check @PL1.theoremA_of_separableSchurLatticeRNP131#print axioms PL1.theoremA_of_separableSchurLatticeRNP132