OAI/Analysis/Pureness/Tensor/SpatialFiniteCompression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.finiteSpatialCoefficients line 15
2. lemma OAI.CuntzPureness.finiteSpatialCoefficients_tmul line 42
3. lemma OAI.CuntzPureness.spatialTensorOp_sum_right line 47
4. theorem OAI.CuntzPureness.spatialFinite_compression line 56
5. theorem OAI.CuntzPureness.finiteSpatialCoefficients_norm_le line 82