OAI/Probability/SignedSweeps/PairWordTypes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.hilbertBlock_intertwine line 15
  2. lemma OAI.SignedSweeps.starProjection_positive line 28
  3. def OAI.SignedSweeps.wordTypeProjection line 51
  4. lemma OAI.SignedSweeps.wordTypeProjection_positive line 56
  5. lemma OAI.SignedSweeps.wordTypeProjection_idempotent line 59
  6. lemma OAI.SignedSweeps.wordTypeProjection_norm_le line 65
  7. lemma OAI.SignedSweeps.wordTypeProjection_tensor_commute line 69
  8. def OAI.SignedSweeps.pairTypeProjection line 81
  9. lemma OAI.SignedSweeps.pairTypeProjection_positive line 87
  10. lemma OAI.SignedSweeps.pairTypeProjection_idempotent line 95
  11. theorem OAI.SignedSweeps.pairTypeProjection_tensor_commute line 113