OAI/Combinatorics/TriangleRemoval/Process/Finish.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.finish line 16
  2. theorem OAI.SharpTerminalLeave.pmf_bind_congr_support line 19
  3. theorem OAI.SharpTerminalLeave.evolve_eq_finish line 31
  4. theorem OAI.SharpTerminalLeave.finish_absorbing line 36
  5. theorem OAI.SharpTerminalLeave.finish_harmonic line 39
  6. def OAI.SharpTerminalLeave.scanAction line 50
  7. def OAI.SharpTerminalLeave.scanLaw line 53
  8. theorem OAI.SharpTerminalLeave.scanAction_subset line 60
  9. theorem OAI.SharpTerminalLeave.triangle_not_mem_delete line 67
  10. theorem OAI.SharpTerminalLeave.triangles_scanAction_subset line 75
  11. theorem OAI.SharpTerminalLeave.finish_mean_uniform_candidates line 87
  12. theorem OAI.SharpTerminalLeave.pmf_ext_mean line 136
  13. theorem OAI.SharpTerminalLeave.scan_mean_eq_finish line 144
  14. theorem OAI.SharpTerminalLeave.scanLaw_eq_finish line 170
  15. theorem OAI.SharpTerminalLeave.scan_complete_eq_terminalLaw line 175