OAI/Analysis/KadisonSimilarity/Similarity/
99 declarations, 0 contain sorry, 0 declared as axioms; 26 files
Files
- AmplifyExponential.lean 5 declarations
- ArvesonCompleteNorm.lean 4 declarations
- ArvesonDischarge.lean 2 declarations
- ArvesonLowerBound.lean 4 declarations
- CompleteNorm.lean 4 declarations
- CompletelyBounded.lean 11 declarations
- CompletelyBoundedImplementation.lean 12 declarations
- CyclicSimilarity.lean 4 declarations
- ExponentialSimilarity.lean 1 declarations
- FiniteCyclicSimilarity.lean 3 declarations
- KirchbergCompleteBound.lean 1 declarations
- KirchbergConjugation.lean 8 declarations
- KirchbergEndgame.lean 2 declarations
- KirchbergExponentialNorm.lean 3 declarations
- KirchbergIntegral.lean 4 declarations
- KirchbergNumerics.lean 2 declarations
- KirchbergScalarDerivation.lean 2 declarations
- KirchbergUniformBound.lean 1 declarations
- Main.lean 7 imports, no declarations
- PaulsenDischarge.lean 2 declarations
- PositiveSimilarity.lean 2 declarations
- SharpCompletelyBoundedDerivation.lean 2 declarations
- SimilarityCompleteBound.lean 5 declarations
- SimilarityMetric.lean 6 declarations
- SimilarityRetract.lean 1 declarations
- SimilarityUniverseTransfer.lean 8 declarations