OAI/Probability/SignedSweeps/TupleRealization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SignedSweeps.InjectiveTuple line 12
  2. def OAI.SignedSweeps.tupleEquiv line 14
  3. lemma OAI.SignedSweeps.tupleEquiv_apply line 21
  4. lemma OAI.SignedSweeps.tupleEquiv_one line 24
  5. lemma OAI.SignedSweeps.tupleEquiv_mul line 27
  6. abbrev OAI.SignedSweeps.TupleSpace line 30
  7. def OAI.SignedSweeps.tupleIsometry line 33
  8. def OAI.SignedSweeps.tupleRepresentation line 37
  9. lemma OAI.SignedSweeps.tupleRepresentation_apply line 50
  10. def OAI.SignedSweeps.extendOffFirstRow line 54
  11. lemma OAI.SignedSweeps.extendOffFirstRow_apply line 58
  12. def OAI.SignedSweeps.tupleRealization line 64
  13. lemma OAI.SignedSweeps.tupleRealization_apply_perm line 70
  14. lemma OAI.SignedSweeps.tupleRealization_injective line 80
  15. lemma OAI.SignedSweeps.tupleRealization_intertwines line 92
  16. lemma OAI.SignedSweeps.tuple_intertwiner_eq_zero_of_fewer_labels line 106
  17. def OAI.SignedSweeps.tupleMarginal line 137
  18. lemma OAI.SignedSweeps.tupleMarginal_intertwines line 152
  19. lemma OAI.SignedSweeps.tupleRealization_marginal_eq_zero line 167