PL1/MainDaugavet.lean

All source files · Download exact source

SHA-256: c0659a45aa16f6e5ba52361ab8fddb61a9c99d7432ce654157acc864dd637470

1import PL1.DaugavetIntrinsicFramework2import PL1.IntrinsicSpikeFamilies3import PL1.ConstantTailSpikes45/-!6# The Daugavet property of both actual intrinsic spaces78The equalities use the original graph ell1 norm of the intrinsic spaces.9They discharge the geometric slice criterion from the actual finite tail10families, without extra concentration, multiplication or averaging premises.11-/1213noncomputable section14open scoped NNReal1516namespace PL1.Noise1718variable (K : Type*) [RCLike K]1920theorem schur_intrinsic_sliceCriterion :21    Daugavet.SliceCriterion K (dyadicSystem K schurRates).IntrinsicSpace :=22  intrinsic_sliceCriterion_of_finiteSpikeFamilies K schurRates23    (IntrinsicSpikeFamilies.finiteSpikeFamilies schurRates24      (fun d T _ hδ => TailSpikes.exists_family d T hδ))2526theorem constant_intrinsic_sliceCriterion :27    Daugavet.SliceCriterion K (dyadicSystem K constantRates).IntrinsicSpace :=28  intrinsic_sliceCriterion_of_finiteSpikeFamilies K constantRates29    (IntrinsicSpikeFamilies.finiteSpikeFamilies constantRates30      (fun d T _ hδ => TailSpikes.exists_constant_family d T hδ))3132theorem schur_intrinsic_hasDaugavetProperty :33    Daugavet.HasDaugavetProperty K (dyadicSystem K schurRates).IntrinsicSpace := by34  let := intrinsicSpace_nontrivial K schurRates35  exact (schur_intrinsic_sliceCriterion K).hasDaugavetProperty3637theorem constant_intrinsic_hasDaugavetProperty :38    Daugavet.HasDaugavetProperty K (dyadicSystem K constantRates).IntrinsicSpace := by39  let := intrinsicSpace_nontrivial K constantRates40  exact (constant_intrinsic_sliceCriterion K).hasDaugavetProperty4142end PL1.Noise43