OAI/Probability/SwitchChain/DisjointStateLaw.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem315.DisjointMarginal.marginData_eq_iff_subset_eq line 14
  2. abbrev OAI.Problem315.DisjointMarginal.StateCell line 32
  3. instance OAI.Problem315.DisjointMarginal.stateCellNonempty line 35
  4. def OAI.Problem315.DisjointMarginal.stateLeftData line 38
  5. def OAI.Problem315.DisjointMarginal.stateRightData line 41
  6. theorem OAI.Problem315.DisjointMarginal.stateLeftData_subset line 44
  7. theorem OAI.Problem315.DisjointMarginal.stateRightData_subset line 47
  8. theorem OAI.Problem315.DisjointMarginal.sameFiber_left_iff_stateRightData_eq line 50
  9. theorem OAI.Problem315.DisjointMarginal.sameFiber_right_iff_stateLeftData_eq line 57
  10. theorem OAI.Problem315.DisjointMarginal.stateCell_of_leftFiber line 64
  11. theorem OAI.Problem315.DisjointMarginal.stateCell_of_rightFiber line 70
  12. def OAI.Problem315.DisjointMarginal.stateCellJointEquiv line 76
  13. theorem OAI.Problem315.DisjointMarginal.stateCell_card_eq line 80
  14. theorem OAI.Problem315.DisjointMarginal.sum_stateCell_joint line 84
  15. theorem OAI.Problem315.DisjointMarginal.stateCell_card_eq_sum_count line 104
  16. theorem OAI.Problem315.DisjointMarginal.average_stateCell_joint line 110
  17. theorem OAI.Problem315.DisjointMarginal.average_stateCell_joint_two line 122
  18. theorem OAI.Problem315.DisjointMarginal.stateCell_joint_fiber_card line 135
  19. theorem OAI.Problem315.DisjointMarginal.stateCell_card_pos line 164
  20. theorem OAI.Problem315.DisjointMarginal.stateCell_mass_two_pos line 167