OAI/Combinatorics/TriangleRemoval/Tracking/TriangleDrift.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.hittingTriangles line 14
  2. def OAI.SharpTerminalLeave.incidentTriangles line 17
  3. def OAI.SharpTerminalLeave.triangleDegree line 21
  4. def OAI.SharpTerminalLeave.intact line 24
  5. theorem OAI.SharpTerminalLeave.pmfMean_sum line 27
  6. theorem OAI.SharpTerminalLeave.step_mean line 33
  7. theorem OAI.SharpTerminalLeave.intact_delete line 39
  8. theorem OAI.SharpTerminalLeave.step_mean_intact line 47
  9. theorem OAI.SharpTerminalLeave.step_mean_intact_of_not_subset line 63
  10. def OAI.SharpTerminalLeave.copyCount line 71
  11. theorem OAI.SharpTerminalLeave.step_mean_copyCount line 75
  12. theorem OAI.SharpTerminalLeave.three_le_card_union line 90
  13. theorem OAI.SharpTerminalLeave.triangle_eq_of_two_edges line 104
  14. theorem OAI.SharpTerminalLeave.sum_card_le_card_biUnion_add_pair_overlaps line 115
  15. theorem OAI.SharpTerminalLeave.hittingTriangles_eq_biUnion line 139
  16. theorem OAI.SharpTerminalLeave.incident_pair_card_le_one line 151
  17. theorem OAI.SharpTerminalLeave.hittingTriangles_card_le_degree_sum line 162
  18. theorem OAI.SharpTerminalLeave.degree_sum_le_hittingTriangles_add line 167
  19. theorem OAI.SharpTerminalLeave.hittingTriangles_degree_error line 187
  20. theorem OAI.SharpTerminalLeave.copyCount_drift_error line 212