OAI/Analysis/JiangSu/CStarAlgebras/
202 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- ActualNormalizedMatching.lean 1 declarations
- AmbientIdealConjugation.lean 8 declarations
- ApproximateUnitSequence.lean 1 declarations
- CStarNormCompletion.lean 6 declarations
- CStarPolarNormalization.lean 10 declarations
- ClosedFunctionAlgebraGluing.lean 2 declarations
- ClosedSubalgebraCP.lean 4 declarations
- CompletedHereditaryWeight.lean 2 declarations
- CompletedRankClosure.lean 5 declarations
- CompletedRankExhaustion.lean 7 declarations
- CompletedRootRank.lean 5 declarations
- ConcreteIterateDiagonalization.lean 7 declarations
- ConnectedStageReduction.lean 1 declarations
- ContinuousOrthogonalSeparation.lean 1 declarations
- ContinuousPositiveEmbedding.lean 7 declarations
- ContinuousRadialFactor.lean 6 declarations
- ContractionLift.lean 1 declarations
- CutoffRank.lean 16 declarations
- EndpointPartition.lean 1 declarations
- EndpointTestCutoffs.lean 1 declarations
- FaithfulGNS.lean 3 declarations
- FiniteDimensionPowers.lean 7 declarations
- FiniteSpectralMatching.lean 3 declarations
- FourEdgeConjugationEstimates.lean 11 declarations
- FourEdgeGroupSurgery.lean 15 declarations
- IsometricHomLimit.lean 3 declarations
- PositiveContractionLift.lean 1 declarations
- SmoothedIntegerCuts.lean 11 declarations
- SourceRankLimit.lean 4 declarations
- StarTerms.lean 5 declarations
- StarTermsNormLift.lean 10 declarations
- StateCoefficientApproximation.lean 14 declarations
- TwoParameterPartition.lean 2 declarations
- UniformTwoNorm.lean 16 declarations
- UnitalKernelCutoff.lean 5 declarations