OAI/Analysis/KadisonSimilarity/Tracial/
970 declarations, 0 contain sorry, 0 declared as axioms; 143 files
Files
- BoundedMatrixHom.lean 4 declarations
- CStarMatrixPadding.lean 17 declarations
- CentralCStarSource.lean 4 declarations
- CofinalMatrixTowers.lean 6 declarations
- ConcreteFiniteFactorModel.lean 5 declarations
- ConcreteFullColumn.lean 6 declarations
- ConcreteGNSNormality.lean 6 declarations
- ConcreteHalfProjection.lean 5 declarations
- ConcreteMatrixTower.lean 20 declarations
- ConcreteProjectionComparison.lean 2 declarations
- ConcreteRealSequence.lean 7 declarations
- ConcreteTracialExpectation.lean 3 declarations
- ConjugateMomentCriterion.lean 9 declarations
- ConstantMomentLimit.lean 2 declarations
- ConstantMomentTransport.lean 1 declarations
- CornerTraceScaling.lean 2 declarations
- DenseMomentExtension.lean 4 declarations
- DiffuseProjectionStructure.lean 1 declarations
- FiniteFactorApplication.lean 3 declarations
- FiniteFactorPresentation.lean 14 declarations
- FiniteFactorSymmetrization.lean 10 declarations
- FiniteFactorTrace.lean 7 declarations
- FullColumnTheorem.lean 32 declarations
- FullColumns.lean 6 declarations
- GNSProjectionContinuity.lean 2 declarations
- GNSSeparableTransport.lean 1 declarations
- GNSTracialGeometry.lean 16 declarations
- GNSVectorDensity.lean 3 declarations
- GeneratedFiniteFactorModel.lean 3 declarations
- GeneratedGNSModels.lean 3 declarations
- GeneratedGNSRecovery.lean 10 declarations
- IntegerMomentMaps.lean 3 declarations
- IntegerMomentScaling.lean 5 declarations
- InternalSourceStages.lean 3 declarations
- IsometricMatrixExtension.lean 1 declarations
- JointCStarSource.lean 11 declarations
- Main.lean 39 imports, no declarations
- MatrixArrayFlattening.lean 35 declarations
- MatrixConjugateAutomorphism.lean 6 declarations
- MatrixCornerFrames.lean 3 declarations
- MatrixDiagonalEmbedding.lean 6 declarations
- MatrixDiffuseSource.lean 2 declarations
- MatrixExpectationIdentification.lean 4 declarations
- MatrixGNSNormality.lean 2 declarations
- MatrixGNSRecovery.lean 7 declarations
- MatrixPopaPosition.lean 4 declarations
- MatrixRelativeCommutant.lean 3 declarations
- MatrixSmallCorner.lean 14 declarations
- MatrixStageGrowth.lean 7 declarations
- MatrixSubfactorTransfer.lean 9 declarations
- MatrixTraceUniqueness.lean 1 declarations
- MatrixTracialGNS.lean 33 declarations
- MatrixTracialInputTransport.lean 1 declarations
- MatrixUnitCoordinates.lean 13 declarations
- MatrixUnitFamilies.lean 23 declarations
- MatrixVonNeumannRange.lean 21 declarations
- NormalRealSequence.lean 1 declarations
- NormalSmallCorners.lean 3 declarations
- NormalTracialExpectations.lean 2 declarations
- NormalTracialGeometry.lean 5 declarations
- NormalTracialInclusionModel.lean 1 declarations
- OppositeTracialGeometry.lean 5 declarations
- PopaConjugatePosition.lean 7 declarations
- PredualGNSNormality.lean 5 declarations
- PredualGNSSeparable.lean 2 declarations
- ProjectionJoinTrace.lean 5 declarations
- ProjectionTraceContinuity.lean 3 declarations
- QuotientMomentLimit.lean 3 declarations
- RelativeMatrixQuantization.lean 7 declarations
- SmallTraceFrames.lean 1 declarations
- SourceAllMoments.lean 1 declarations
- SourceConstantMoments.lean 1 declarations
- SourceCornerQuantization.lean 9 declarations
- SourceIncrementalPatching.lean 1 declarations
- SourceLocalQuantization.lean 1 declarations
- SourceMomentConstruction.lean 2 declarations
- SourceMomentSequence.lean 1 declarations
- SourcePartialUnitaries.lean 7 declarations
- SourceQuotientMoments.lean 3 declarations
- SourceUltrapowerInclusion.lean 2 declarations
- SourceUnitaryMoments.lean 1 declarations
- SourceWeakPowers.lean 3 declarations
- TraceDenseContractions.lean 1 declarations
- TracialAdjointBounds.lean 2 declarations
- TracialAutomorphisms.lean 11 declarations
- TracialBaseGeometry.lean 12 declarations
- TracialBaseSpace.lean 28 declarations
- TracialBoundedBalls.lean 3 declarations
- TracialCommutantTrace.lean 8 declarations
- TracialCommutationDischarge.lean 1 declarations
- TracialCornerEstimate.lean 4 declarations
- TracialCornerExpectations.lean 11 declarations
- TracialCornerHilbert.lean 12 declarations
- TracialCornerRepresentations.lean 10 declarations
- TracialCornerTransport.lean 6 declarations
- TracialCreationCoordinates.lean 9 declarations
- TracialEmbeddingBalls.lean 3 declarations
- TracialEmbeddingTransport.lean 8 declarations
- TracialExpectations.lean 16 declarations
- TracialFactorComparison.lean 2 declarations
- TracialGeneratedAlgebra.lean 2 declarations
- TracialGeneratedNormalClosure.lean 3 declarations
- TracialGeometrySupport.lean 3 declarations
- TracialGraphClosability.lean 2 declarations
- TracialHalfProjectionData.lean 17 declarations
- TracialHeadCoordinates.lean 7 declarations
- TracialIncludedCorners.lean 1 declarations
- TracialInclusionModel.lean 2 declarations
- TracialInclusionNormality.lean 7 declarations
- TracialInclusionQuantization.lean 5 declarations
- TracialInputTransport.lean 13 declarations
- TracialL2Closure.lean 23 declarations
- TracialMatrixCenter.lean 3 declarations
- TracialMatrixColumns.lean 12 declarations
- TracialMatrixCovariance.lean 20 declarations
- TracialMatrixDiffuse.lean 1 declarations
- TracialMatrixRealization.lean 30 declarations
- TracialMatrixSymmetrization.lean 21 declarations
- TracialMatrixTower.lean 17 declarations
- TracialMomentContinuity.lean 6 declarations
- TracialNormalSpan.lean 5 declarations
- TracialNormalityCriterion.lean 1 declarations
- TracialProjectionLifting.lean 4 declarations
- TracialRightSupportDischarge.lean 3 declarations
- TracialSmallColumn.lean 10 declarations
- TracialSmallCornerTransfer.lean 8 declarations
- TracialSpectralColumns.lean 2 declarations
- TracialSpectralNorm.lean 3 declarations
- TracialSpectralTest.lean 1 declarations
- TracialStageCommutation.lean 6 declarations
- TracialSubalgebraModels.lean 8 declarations
- TracialSubalgebraTransfer.lean 4 declarations
- TracialSupportedColumns.lean 13 declarations
- TracialUltrapowerActions.lean 7 declarations
- TracialUltrapowerConstants.lean 4 declarations
- TracialUltrapowerCorners.lean 1 declarations
- TracialUltrapowerGNS.lean 9 declarations
- TracialUltrapowerHom.lean 7 declarations
- UltrapowerCommutators.lean 3 declarations
- UltrapowerConstants.lean 8 declarations
- UltrapowerGeneratedTransfer.lean 4 declarations
- UltrapowerNormality.lean 2 declarations
- UltrapowerTraceBalls.lean 2 declarations