OAI/Combinatorics/TriangleRemoval/Probability/ProductPMF.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.productPMF line 14
  2. theorem OAI.SharpTerminalLeave.productPMF_apply line 25
  3. theorem OAI.SharpTerminalLeave.productPMF_support line 28
  4. theorem OAI.SharpTerminalLeave.productPMF_update_apply line 33
  5. theorem OAI.SharpTerminalLeave.productPMF_split line 47
  6. inductive OAI.SharpTerminalLeave.ExposureTree line 61
  7. def OAI.SharpTerminalLeave.ExposureTree.evaluate line 68
  8. def OAI.SharpTerminalLeave.ExposureTree.fresh line 72
  9. def OAI.SharpTerminalLeave.ExposureTree.coupled line 76
  10. theorem OAI.SharpTerminalLeave.ExposureTree.coupled_agrees line 84
  11. def OAI.SharpTerminalLeave.ExposureTree.freshRecorded line 99
  12. theorem OAI.SharpTerminalLeave.ExposureTree.freshRecorded_outcome line 107
  13. theorem OAI.SharpTerminalLeave.pmf_bind_congr_on_support line 124
  14. theorem OAI.SharpTerminalLeave.ExposureTree.coupled_independent_law line 137
  15. theorem OAI.SharpTerminalLeave.ExposureTree.coupled_independent_law_empty line 173
  16. def OAI.SharpTerminalLeave.ExposureTree.jointLaw line 177
  17. theorem OAI.SharpTerminalLeave.ExposureTree.jointLaw_fixed line 184
  18. theorem OAI.SharpTerminalLeave.ExposureTree.jointLaw_fresh line 192
  19. theorem OAI.SharpTerminalLeave.ExposureTree.jointLaw_agrees line 201