OAI/Analysis/JiangSu/Excision/
135 declarations, 0 contain sorry, 0 declared as axioms; 18 files
Files
- ExcisionCoefficientAssembly.lean 10 declarations
- ExcisionFullnessError.lean 7 declarations
- ExcisionSoftCompression.lean 19 declarations
- ExcisionTraceProjection.lean 1 declarations
- ExcisionUpperCut.lean 19 declarations
- FiniteIdentityExcision.lean 1 declarations
- FiniteNuclearIdentityExcision.lean 5 declarations
- JordanDomination.lean 5 declarations
- OrthogonalExcision.lean 4 declarations
- PureGNSCommutant.lean 8 declarations
- PureGNSProjections.lean 9 declarations
- PureGNSStrongDensity.lean 8 declarations
- PureStateCarrier.lean 18 declarations
- PureStateExcision.lean 8 declarations
- PureStateExcisionNormUltrapower.lean 2 declarations
- PureStateNorming.lean 3 declarations
- PureStateOrthogonalExtension.lean 6 declarations
- PureStateSmallExcision.lean 2 declarations