OAI/Analysis/Pureness/Tensor/SpatialPartialTranslations.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.sum_mul_star_sum_of_orthogonal line 11
  2. abbrev OAI.CuntzPureness.spatialPartialOperatorOrder line 22
  3. abbrev OAI.CuntzPureness.spatialPartialOperatorStarOrdered line 28
  4. lemma OAI.CuntzPureness.spatialTensorOp_sub_right line 36
  5. def OAI.CuntzPureness.spatialLetterSum line 43
  6. lemma OAI.CuntzPureness.spatialLetterSum_compressions line 47
  7. lemma OAI.CuntzPureness.spatialLetterSum_nonneg line 58
  8. lemma OAI.CuntzPureness.spatialPartialLeft_norm_le line 69
  9. lemma OAI.CuntzPureness.spatialLetterSum_norm_le line 77
  10. def OAI.CuntzPureness.spatialFreeCreationSum line 92
  11. def OAI.CuntzPureness.spatialFreeCancellationSum line 95
  12. lemma OAI.CuntzPureness.spatialFreeTranslation_split line 99
  13. lemma OAI.CuntzPureness.spatialFreeCreationSum_square line 108
  14. lemma OAI.CuntzPureness.spatialFreeCancellationSum_square line 126