OAI/Analysis/Pureness/Comparison/

Files

• Comparison.lean 9 declarations
• ComparisonCornerCompression.lean 3 declarations
• ComparisonIsometry.lean 2 declarations
• CuntzCornerReflection.lean 1 declarations
• FaithfulGNS.lean 3 declarations
• FaithfulTrace.lean 9 declarations
• FiniteOrthogonalSupply.lean 2 declarations
• FiniteRootCompatibility.lean 2 declarations
• Fullness.lean 8 declarations
• FullnessFrame.lean 5 declarations
• HereditaryApproximation.lean 5 declarations
• HereditaryCorner.lean 13 declarations
• HereditarySupportMass.lean 4 declarations
• IntegerCuts.lean 5 declarations
• MatrixCornerFunctionals.lean 11 declarations
• MatrixDiagonal.lean 7 declarations
• MatrixExtendedTrace.lean 11 declarations
• MatrixRankApproximation.lean 1 declarations
• MatrixTrace.lean 10 declarations
• MatrixTraceCompression.lean 5 declarations
• MatrixTraceValues.lean 14 declarations
• MatrixUnitCorners.lean 6 declarations
• OrthogonalSupply.lean 4 declarations
• OrthogonalSupportMass.lean 5 declarations
• PositiveReflection.lean 1 declarations
• RankCutFamily.lean 1 declarations
• RootRankIdentification.lean 6 declarations
• ScalarCorners.lean 3 declarations
• SpatialCompactTensor.lean 8 declarations
• SpatialCompletion.lean 11 declarations
• SpatialFiniteMatrices.lean 21 declarations
• SpatialIdentification.lean 14 declarations
• SpatialTensorOperators.lean 14 declarations
• SpatialTrace.lean 9 declarations
• SpectralIntegration.lean 10 declarations
• SpectralMeasure.lean 11 declarations
• SpectralSplitting.lean 3 declarations
• SpectralTransport.lean 6 declarations
• SupportApproximation.lean 12 declarations
• ThinSpectralSupport.lean 2 declarations
• TraceAlgebra.lean 10 declarations
• TraceBounds.lean 6 declarations
• TraceCompressionExistence.lean 3 declarations
• TraceFunctionalCalculus.lean 4 declarations
• TraceNullIdeal.lean 12 declarations
• TracialExtendedTrace.lean 3 declarations
• TracialState.lean 15 declarations
• UniformTwoNorm.lean 16 declarations