OAI/Analysis/TracialSplitting/
1182 declarations, 0 contain sorry, 0 declared as axioms; 51 files
Files
- BistochasticTests.lean 13 declarations
- BlockAveraging.lean 8 declarations
- BlockSampling.lean 4 declarations
- Challenge.lean 4 declarations
- ChallengeDefinitions.lean 67 declarations
- CoefficientApproximation.lean 10 declarations
- CoefficientBounds.lean 17 declarations
- Completion.lean 43 declarations
- ConditionalSplitting.lean 10 declarations
- Diagonalization.lean 11 declarations
- FaithfulRepresentations.lean 28 declarations
- FinitePacking.lean 17 declarations
- FiniteSplitting.lean 1 declarations
- FullProjections.lean 15 declarations
- GNSRepresentations.lean 18 declarations
- HereditaryAlgebras.lean 20 declarations
- Hypertraces.lean 9 declarations
- KrausApproximation.lean 17 declarations
- Main.lean 1 declarations
- MatrixCoefficients.lean 30 declarations
- MatrixNormalization.lean 35 declarations
- Model.lean 126 declarations
- NuclearApproximation.lean 9 declarations
- NuclearFamilies.lean 2 declarations
- NuclearPacking.lean 1 declarations
- NuclearTransfer.lean 8 declarations
- OrthogonalElements.lean 25 declarations
- OrthogonalPacking.lean 29 declarations
- PackingEstimates.lean 56 declarations
- PartitionAveraging.lean 4 declarations
- PartitionCoupling.lean 27 declarations
- PreparedBlocks.lean 4 declarations
- ProjectionFrames.lean 28 declarations
- ProjectionRounding.lean 18 declarations
- ProjectionSampling.lean 41 declarations
- RowEstimates.lean 42 declarations
- ScalarCompression.lean 25 declarations
- SimpleIdeals.lean 44 declarations
- SmallProjections.lean 2 declarations
- SpatialTensor.lean 23 declarations
- SpectralBlocks.lean 26 declarations
- SpectralCutoffs.lean 56 declarations
- SpectralLayers.lean 51 declarations
- StateExtension.lean 16 declarations
- TensorExtension.lean 7 declarations
- TensorNorms.lean 4 declarations
- TraceConvexity.lean 10 declarations
- TraceEstimates.lean 58 declarations
- TraceNormalization.lean 21 declarations
- VectorApproximation.lean 22 declarations
- WeightedFamilies.lean 19 declarations