OAI/Analysis/NuclearUltrapower/
7803 declarations, 0 contain sorry, 0 declared as axioms; 39 files
Files
- CuntzAlgebra.lean 69 declarations
- CuntzIntertwining.lean 35 declarations
- CuntzNuclearity.lean 13 declarations
- CuntzWords.lean 39 declarations
- DyadicGroup.lean 26 declarations
- FaithfulGNS.lean 16 declarations
- FiniteInduction.lean 29 declarations
- FiniteRepresentations.lean 26 declarations
- FullGroupAlgebra.lean 52 declarations
- GroupObstruction.lean 6 declarations
- HilbertInduction.lean 26 declarations
- HilbertSchmidt.lean 87 declarations
- HilbertTensor.lean 25 declarations
- HilbertUltraproduct.lean 30 declarations
- InducedApproximation.lean 36 declarations
- InitialMatching.lean 6 declarations
- IntegerMatrices.lean 42 declarations
- IntegralCertificate.lean 45 declarations
- Kazhdan.lean 73 declarations
- Laplacian.lean 7 declarations
- Main.lean 1 declarations
- ModTwo.lean 16 declarations
- Model.lean 29 declarations
- NormUltrapower.lean 22 declarations
- NuclearFiniteness.lean 60 declarations
- Obstruction.lean 6 declarations
- Predecessors.lean 4 declarations
- PullbackMatching.lean 22 declarations
- RepresentationUltraproduct.lean 6 declarations
- SOSCertificate.lean 369 declarations
- SOSGap.lean 28 declarations
- SOSResidual.lean 6351 declarations
- SOSSemantics.lean 31 declarations
- Schur.lean 15 declarations
- SpatialGap.lean 14 declarations
- TensorGap.lean 38 declarations
- TensorMatching.lean 23 declarations
- TensorNorms.lean 30 declarations
- VariableUltraproduct.lean 50 declarations