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

PL1/SecondProofReview.lean

All source files · Download exact source

SHA-256: 38b1d93c35d223743f5071f676d4af4892edb61d0faff0f8332083a2df98fc03

1import PL1.MainTheoremA2import PL1.MainDaugavet3import PL1.DaugavetRealification4import PL1.IntrinsicExposedPoint5import PL1.IntrinsicTailNorm6import PL1.ExplicitMartingaleFiltration7import PL1.ExplicitMartingaleWeak8import PL1.ConstantNoiseTrace9import PL1.ComplementedLatticeRealAmbient10import PL1.NoiseGeneratorCore11import PL1.GeneratorGraphBanach12import PL1.ExtendedDiscreteInterpolation13import PL1.MainInterpolation14import PL1.InterpolationBochner15import PL1.InterpolationNorm16import PL1.DaugavetDiameter17import PL1.SummingTransport1819/-!20# Exact type and axiom audit for the second three-hour pass2122The original A targets below are proved without added hypotheses. The full B23endpoint remains conditional on three explicitly printed real structural24premises. All geometry uses the original intrinsic norm. These ordinary Lean25checks and axiom reports complement the independent semantic audits.26-/2728set_option pp.universes true2930example : PL1.TheoremARealStatement := PL1.theoremAReal31example : PL1.TheoremAComplexStrongStatement := PL1.theoremAComplexStrong3233#check @PL1.theoremA34#print PL1.TheoremAStatement35#print PL1.TheoremAComplexStrongStatement36#print axioms PL1.separableSchurLatticeRNP37#print axioms PL1.theoremA38#print axioms PL1.theoremAReal39#print axioms PL1.theoremAComplexStrong4041#print PL1.ComplementedLattice.ComplementedL1LatticeClassification42#print PL1.ComplementedLattice.SeparableRealL1Dichotomy43#print PL1.ComplementedLattice.L1CopyExtraction44#check @PL1.ComplementedLattice.theoremB_real_and_complex_of_real_structural_properties45#print axioms PL1.ComplementedLattice.theoremB_real_and_complex_of_real_structural_properties46#print axioms PL1.ComplementedLattice.scalarIntervalRealCopy4748#check @PL1.NoiseHypercontractivity.positiveTimeNoiseL249#check @PL1.NoiseHypercontractivity.positiveTimeNoiseL2_overlap50#print axioms PL1.NoiseHypercontractivity.norm_positiveTimeNoiseL2_le_one51#print axioms PL1.NoiseHypercontractivity.positiveTimeNoiseL2_overlap52#print axioms PL1.NoiseHypercontractivity.exponent_lt_two53#check @PL1.Noise.constant_intervalProjection_hasVanishingDyadicTrace54#print axioms PL1.Noise.constant_resolvent_hasVanishingDyadicTrace55#print axioms PL1.Noise.constant_projection_hasVanishingDyadicTrace56#print axioms PL1.Noise.constant_intervalProjection_hasVanishingDyadicTrace57#print axioms PL1.Noise.constant_intervalProjection_identity_distance58#print axioms PL1.Noise.constant_intervalProjection_not_factors_identity5960#print PL1.Daugavet.HasDaugavetProperty61#check PL1.Noise.schur_intrinsic_hasDaugavetProperty ℝ62#check PL1.Noise.schur_intrinsic_hasDaugavetProperty ℂ63#check PL1.Noise.constant_intrinsic_hasDaugavetProperty ℝ64#check PL1.Noise.constant_intrinsic_hasDaugavetProperty ℂ65#check PL1.Noise.schur_intrinsic_underlyingReal_hasDaugavetProperty ℂ66#check PL1.Noise.constant_intrinsic_underlyingReal_hasDaugavetProperty ℂ67#print axioms PL1.Noise.schur_intrinsic_hasDaugavetProperty68#print axioms PL1.Noise.constant_intrinsic_hasDaugavetProperty69#print axioms PL1.Noise.schur_intrinsic_underlyingReal_hasDaugavetProperty70#print axioms PL1.Noise.constant_intrinsic_underlyingReal_hasDaugavetProperty7172#check @PL1.IntrinsicTailNorm.schur_norm_id_sub_intrinsicExpectation_eq_two73#check @PL1.IntrinsicTailNorm.constant_norm_id_sub_intrinsicExpectation_eq_two74#print axioms PL1.IntrinsicTailNorm.schur_norm_id_sub_intrinsicExpectation_eq_two75#print axioms PL1.IntrinsicTailNorm.constant_norm_id_sub_intrinsicExpectation_eq_two76#check @PL1.IntrinsicExposedPoint.integralFunctional_maximum_iff77#check @PL1.IntrinsicExposedPoint.integralFunctional_strict_maximum78#print axioms PL1.IntrinsicExposedPoint.norm_integralFunctional79#print axioms PL1.IntrinsicExposedPoint.schur_integralFunctional_exposes_constant80#print axioms PL1.IntrinsicExposedPoint.constant_integralFunctional_exposes_constant8182#check PL1.ExplicitMartingale.schur_explicit_martingale ℝ83#check PL1.ExplicitMartingale.schur_explicit_martingale ℂ84#check PL1.ExplicitMartingale.constant_explicit_martingale ℝ85#check PL1.ExplicitMartingale.constant_explicit_martingale ℂ86#check @PL1.ExplicitMartingale.schur_beta_exists_dual_oscillation87#check @PL1.ExplicitMartingale.schur_beta_not_weaklyCauchy_real88#print axioms PL1.ExplicitMartingale.schur_explicit_martingale89#print axioms PL1.ExplicitMartingale.constant_explicit_martingale90#print axioms PL1.ExplicitMartingale.schur_beta_exists_dual_oscillation91#print axioms PL1.ExplicitMartingale.schur_beta_not_weaklyCauchy_real9293#print PL1.Noise.IsGeneratorPair94#check @PL1.Noise.isGeneratorPair_iff_mem_graph95#check @PL1.Noise.IsGeneratorPair.polynomial_core96#check @PL1.GeneratorGraphBanach.norm_eq97#check @PL1.GeneratorGraphBanach.kFunctional_eq98#print axioms PL1.Noise.isGeneratorPair_iff_mem_graph99#print axioms PL1.Noise.dense_generator_domain100#print axioms PL1.Noise.isClosed_generator_graph101#print axioms PL1.Noise.IsGeneratorPair.polynomial_core102#print axioms PL1.GeneratorGraphBanach.norm_eq103#print axioms PL1.GeneratorGraphBanach.kFunctional_eq104#print axioms PL1.KFunctional.half_norm_defect_le105#print axioms PL1.KFunctional.value_le_defect106#print axioms PL1.DiscreteInterpolation.mem_range_evalZero_iff107#print axioms PL1.DiscreteInterpolation.half_norm_le108#print axioms PL1.DiscreteInterpolation.normValue_le109#print axioms PL1.DiscreteInterpolation.extendedNorm_ne_top_iff110111#print PL1.Interpolation.normIntegral112#check @PL1.Interpolation.intrinsic_eq_realInterpolation113#check PL1.Interpolation.intrinsic_eq_realInterpolation ℝ PL1.Noise.schurRates114#check PL1.Interpolation.intrinsic_eq_realInterpolation ℂ PL1.Noise.schurRates115#check PL1.Interpolation.intrinsic_eq_realInterpolation ℝ PL1.Noise.constantRates116#check PL1.Interpolation.intrinsic_eq_realInterpolation ℂ PL1.Noise.constantRates117#print axioms PL1.KFunctional.continuousNorm_le_four_extendedNorm118#print axioms PL1.KFunctional.extendedNorm_le_five_continuousNorm119#print axioms PL1.Interpolation.mem_intrinsic_iff120#print axioms PL1.Interpolation.normValue_lower121#print axioms PL1.Interpolation.normValue_upper122#print axioms PL1.Interpolation.intrinsic_eq_realInterpolation123124#check @PL1.Interpolation.mem_intrinsic_iff_integrable125#check @PL1.Interpolation.normValue_eq_integral126#check @PL1.InterpolationNorm.continuousLinearEquiv127#check @PL1.InterpolationNorm.norm_eq_integral128#print axioms PL1.Interpolation.mem_intrinsic_iff_integrable129#print axioms PL1.Interpolation.normValue_eq_integral130#print axioms PL1.KFunctional.continuousNorm_add_le131#print axioms PL1.KFunctional.continuousNorm_smul132#print axioms PL1.KFunctional.continuousNorm_eq_zero_iff133#print axioms PL1.InterpolationNorm.continuousLinearEquiv134#print axioms PL1.InterpolationNorm.norm_eq_integral135#print axioms PL1.InterpolationNorm.inclusion_injective136137example : CompleteSpace (PL1.InterpolationNorm.Space ℝ PL1.Noise.schurRates) := inferInstance138example : CompleteSpace (PL1.InterpolationNorm.Space ℂ PL1.Noise.constantRates) := inferInstance139140-- Importing the dedicated interpolation norm leaves the original norm intact.141example (K : Type*) [RCLike K] (rates : ℕ → NNReal)142    (x : (PL1.Noise.dyadicSystem K rates).IntrinsicSpace) :143    ‖x‖ = ∑' n, ‖PL1.IntrinsicGraph.coord (PL1.Noise.dyadicSystem K rates).analysis n x‖ :=144  PL1.IntrinsicGraph.norm_eq_tsum _ x145146#check @PL1.Daugavet.SliceCriterion.diam_realPartSlice147#check @PL1.Daugavet.SliceCriterion.not_strongly_exposes148#check @PL1.Noise.schur_intrinsic_integral_maximizing_sequence_far149#check @PL1.Noise.constant_intrinsic_integral_maximizing_sequence_far150#print axioms PL1.Daugavet.SliceCriterion.diam_realPartSlice151#print axioms PL1.Daugavet.SliceCriterion.not_strongly_exposes152#print axioms PL1.Noise.schur_intrinsic_underlyingReal_diam_realPartSlice153#print axioms PL1.Noise.constant_intrinsic_underlyingReal_diam_realPartSlice154#print axioms PL1.Noise.schur_intrinsic_integral_maximizing_sequence_far155#print axioms PL1.Noise.constant_intrinsic_integral_maximizing_sequence_far156157-- The ambient summing bounds and principal projections remain explicit inputs.158#check @PL1.ComplementedLattice.OneSummingWith.precomp159#check @PL1.ComplementedLattice.OneSummingWith.postcomp160#check @PL1.ComplementedLattice.TwoSummingWith.precomp161#check @PL1.ComplementedLattice.TwoSummingWith.postcomp162#check @PL1.ComplementedLattice.uniform_finite_summing_estimates163#check @PL1.ComplementedLattice.disjoint_sum_norm_le_of_complemented_ambient_estimates164#print axioms PL1.ComplementedLattice.OneSummingWith.precomp165#print axioms PL1.ComplementedLattice.OneSummingWith.postcomp166#print axioms PL1.ComplementedLattice.TwoSummingWith.precomp167#print axioms PL1.ComplementedLattice.TwoSummingWith.postcomp168#print axioms PL1.ComplementedLattice.uniform_finite_summing_estimates169#print axioms PL1.ComplementedLattice.disjoint_sum_norm_le_of_complemented_ambient_estimates170