OAI/Probability/SwitchChain/DisjointCellCounting.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.DisjointMarginal.MarginData line 14
  2. abbrev OAI.Problem315.DisjointMarginal.LeftData line 17
  3. abbrev OAI.Problem315.DisjointMarginal.RightData line 21
  4. abbrev OAI.Problem315.DisjointMarginal.MatrixFiber line 25
  5. abbrev OAI.Problem315.DisjointMarginal.JointData line 29
  6. def OAI.Problem315.DisjointMarginal.leftData line 33
  7. def OAI.Problem315.DisjointMarginal.rightData line 40
  8. def OAI.Problem315.DisjointMarginal.toJointData line 47
  9. def OAI.Problem315.DisjointMarginal.fromJointData line 53
  10. def OAI.Problem315.DisjointMarginal.coordinatesEquiv line 66
  11. def OAI.Problem315.DisjointMarginal.degreeCellJointEquiv line 78
  12. theorem OAI.Problem315.DisjointMarginal.matrixFiber_card line 82
  13. theorem OAI.Problem315.DisjointMarginal.sum_degreeCell_joint line 86
  14. theorem OAI.Problem315.DisjointMarginal.card_degreeCell_eq_sum_count line 107
  15. theorem OAI.Problem315.DisjointMarginal.average_degreeCell_joint line 113
  16. def OAI.Problem315.DisjointMarginal.flag line 126
  17. theorem OAI.Problem315.DisjointMarginal.flag_zero_or_one line 128
  18. theorem OAI.Problem315.DisjointMarginal.sum_degreeCell_joint_two line 132
  19. theorem OAI.Problem315.DisjointMarginal.card_degreeCell_eq_mass_two line 148
  20. theorem OAI.Problem315.DisjointMarginal.average_degreeCell_joint_two line 156