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

PL1.lean

All source files · Download exact source

SHA-256: 7e5b4925d5fa6c299eae8ec742de23c927a49c3433e41b393ae71a095cbf4c94

1import PL1.ALAlternative2import PL1.ALAtomic3import PL1.ALDyadicEmbedding4import PL1.ALFragments5import PL1.ALOrder6import PL1.ALRenorming7import PL1.AtomicBandDecomposition8import PL1.BalancedFragmentTree9import PL1.BochnerResolvents10import PL1.BonamiHaarBridge11import PL1.BonamiTensorization12import PL1.BonamiTwoPoint13import PL1.CarrierAsymptotics14import PL1.CompactRestriction15import PL1.CompactWalshMultiplier16import PL1.ComplementedLatticeBandEstimates17import PL1.ComplementedLatticeRealAmbient18import PL1.ComplementedLatticeRealTrace19import PL1.ComplementedLatticeReduction20import PL1.ComplementedLatticeSumming21import PL1.ConcreteResolvents22import PL1.ConstantNoiseTrace23import PL1.ConstantTailSpikes24import PL1.ConvolutionHypercontractivity25import PL1.ConvolutionL126import PL1.DaugavetAveraging27import PL1.DaugavetCriterion28import PL1.DaugavetDiameter29import PL1.DaugavetIntrinsicFramework30import PL1.DaugavetRealification31import PL1.DecompositionRNP32import PL1.Definitions33import PL1.DiscreteInterpolation34import PL1.DisjointNormingFunctionals35import PL1.DunfordPettis36import PL1.DyadicCellMeasure37import PL1.DyadicCoordinateDomination38import PL1.DyadicInterpolationIntegral39import PL1.DyadicInterpolationNormComparison40import PL1.DyadicL1Coordinates41import PL1.DyadicProjection42import PL1.DyadicSchur43import PL1.DyadicTrace44import PL1.EigenvectorEmbedding45import PL1.Ell1RNP46import PL1.Ell2Schur47import PL1.EnfloBush48import PL1.EnfloCopyExclusion49import PL1.EnfloDyadicDecay50import PL1.EnfloHypercontractive51import PL1.EnfloIntrinsic52import PL1.EnfloMajorant53import PL1.EnfloMaxMass54import PL1.EnfloNoL155import PL1.EnfloSmoothing56import PL1.EnfloStarbirdDyadic57import PL1.EnfloStarbirdProjection58import PL1.EnfloSum59import PL1.EnfloTruncation60import PL1.EnfloTwoMaps61import PL1.EnfloVanishing62import PL1.ExplicitMartingale63import PL1.ExplicitMartingaleFiltration64import PL1.ExplicitMartingaleWeak65import PL1.ExponentialTail66import PL1.ExponentialTime67import PL1.ExtendedDiscreteInterpolation68import PL1.FiniteCoordinateKernels69import PL1.FiniteDimensionalRNP70import PL1.FiniteDualDisjointization71import PL1.FiniteGrothendieck72import PL1.FiniteGrothendieckNormalization73import PL1.FiniteRademacherClipping74import PL1.FiniteSummingFromMatrix75import PL1.GeneratorGraphBanach76import PL1.HeadTail77import PL1.HeadTailNoise78import PL1.HeadTailNorms79import PL1.HilbertDyadicTrace80import PL1.HilbertTraceBounds81import PL1.InputCompression82import PL1.InterpolationBochner83import PL1.InterpolationNorm84import PL1.IntervalDyadicApproximation85import PL1.IntervalEll1Obstruction86import PL1.IntervalModel87import PL1.IntervalRetraction88import PL1.IntervalSubtype89import PL1.IntervalSumming90import PL1.IntervalWalsh91import PL1.IntrinsicApproximations92import PL1.IntrinsicExposedPoint93import PL1.IntrinsicGraph94import PL1.IntrinsicHeadRepresentatives95import PL1.IntrinsicNonBoundedComplete96import PL1.IntrinsicRealParts97import PL1.IntrinsicSpikeAverages98import PL1.IntrinsicSpikeEstimates99import PL1.IntrinsicSpikeFamilies100import PL1.IntrinsicSpikes101import PL1.IntrinsicTailNorm102import PL1.IntrinsicWalsh103import PL1.IntrinsicWalshBlocks104import PL1.KernelL1105import PL1.KernelTranslations106import PL1.KFunctional107import PL1.KFunctionalIntegral108import PL1.KFunctionalIntegralMeasurable109import PL1.KFunctionalNormLaws110import PL1.KFunctionalProperties111import PL1.L1Masks112import PL1.L1Multiplication113import PL1.L1Sum114import PL1.L1Truncation115import PL1.L1UniformIntegrability116import PL1.LatticeAbsoluteContinuity117import PL1.LatticeAtoms118import PL1.LatticeBridge119import PL1.LatticeDefinitions120import PL1.LatticeDisjointCountability121import PL1.LatticeFragments122import PL1.LatticeRademacher123import PL1.LatticeRademacherWeak124import PL1.LatticeReduction125import PL1.LatticeRenorming126import PL1.LatticeStrictPositive127import PL1.LpInclusions128import PL1.LpInterpolation129import PL1.LpOperatorLift130import PL1.MainDaugavet131import PL1.MainInterpolation132import PL1.MainTheoremA133import PL1.MainTheoremB134import PL1.MatrixSmoothing135import PL1.MatrixTrace136import PL1.MatrixTraceLimit137import PL1.MetricApproximation138import PL1.NoiseGenerator139import PL1.NoiseGeneratorCore140import PL1.NoiseHypercontractivity141import PL1.NoiseMeasures142import PL1.NoiseSemigroup143import PL1.NoiseTraceObstruction144import PL1.NonSchurExample145import PL1.OperatorDomination146import PL1.OutputCompression147import PL1.PartialMainTheorems148import PL1.PartitionAverages149import PL1.PositiveLowerOneBridge150import PL1.PrincipalIdealDual151import PL1.ProjectionRetract152import PL1.ProjectionTransport153import PL1.RademacherEmbedding154import PL1.RealSchur155import PL1.ResolventAlmostInvariant156import PL1.ResolventEstimates157import PL1.ResolventGeneratorGraph158import PL1.ResolventMultiplication159import PL1.ResolventNorms160import PL1.RNPBridge161import PL1.RNPTransport162import PL1.ScalarDecompositionRNP163import PL1.ScalarRealification164import PL1.ScalarUnconditionalRNP165import PL1.SchurApproximation166import PL1.SchurBoundedCompleteness167import PL1.SchurExample168import PL1.SchurLattice169import PL1.SchurLatticeAtomicity170import PL1.SchurLatticeCompactness171import PL1.SeparableRange172import PL1.SingularCarrier173import PL1.SingularConvolution174import PL1.SingularResolvents175import PL1.SmoothingApproximation176import PL1.SmoothingTrace177import PL1.SpikeSeparation178import PL1.Statements179import PL1.StrongConvergence180import PL1.SummingTransport181import PL1.TailSpikeEvents182import PL1.TailSpikeMultiplication183import PL1.TailSpikes184import PL1.TraceBounds185import PL1.TraceDomination186import PL1.TraceVanishing187import PL1.TruncatedResolventFactorization188import PL1.UnconditionalDecomposition189import PL1.UnconditionalRNP190import PL1.VectorDensityBounds191import PL1.WalshBlocks192import PL1.WalshExpectations193import PL1.WalshModel194import PL1.WeakSchur195import PL1.WeakSequentialCompleteness196import PL1.WeightedL1197