OAI/Probability/SignedSweeps/GroupedTypes.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.groupedWordOperator_one line 14
  2. lemma OAI.SignedSweeps.groupedWordOperator_sum line 18
  3. lemma OAI.SignedSweeps.groupedWordOperator_zero_factor line 32
  4. def OAI.SignedSweeps.blockTypeProjection line 42
  5. def OAI.SignedSweeps.blockEntropy line 46
  6. lemma OAI.SignedSweeps.blockTypeProjection_sum line 48
  7. lemma OAI.SignedSweeps.blockTypeProjection_positive line 54
  8. lemma OAI.SignedSweeps.blockTypeProjection_idempotent line 57
  9. lemma OAI.SignedSweeps.blockTypeProjection_global_commute line 61
  10. lemma OAI.SignedSweeps.blockTypeProjection_coefficient_commute line 67
  11. lemma OAI.SignedSweeps.blockTypeProjection_zero_of_height line 74
  12. lemma OAI.SignedSweeps.blockTypeProjection_trace line 81