OAI/Combinatorics/TriangleRemoval/Tracking/PrefixEpsilon.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.prefixEpsilon line 14
  2. def OAI.SharpTerminalLeave.prefixCycleCap line 15
  3. def OAI.SharpTerminalLeave.prefixSuffixLength line 16
  4. def OAI.SharpTerminalLeave.prefixSuppression line 17
  5. def OAI.SharpTerminalLeave.prefixTemplateCap line 18
  6. def OAI.SharpTerminalLeave.prefixTargetDensity line 20
  7. def OAI.SharpTerminalLeave.prefixTargetTime line 23
  8. def OAI.SharpTerminalLeave.prefixTime line 26
  9. def OAI.SharpTerminalLeave.prefixDensity line 28
  10. def OAI.SharpTerminalLeave.prefixD line 31
  11. def OAI.SharpTerminalLeave.prefixM line 32
  12. def OAI.SharpTerminalLeave.prefixLaw line 34
  13. def OAI.SharpTerminalLeave.neighbors line 37
  14. def OAI.SharpTerminalLeave.currentDegree line 40
  15. def OAI.SharpTerminalLeave.cycleNext line 43
  16. def OAI.SharpTerminalLeave.linkCycleCount line 46
  17. def OAI.SharpTerminalLeave.largeTemplateEligible line 51
  18. def OAI.SharpTerminalLeave.smallTemplateEligible line 56
  19. def OAI.SharpTerminalLeave.prefixTemplateFactor line 60
  20. def OAI.SharpTerminalLeave.GoodPrefixGraph line 63
  21. def OAI.SharpTerminalLeave.prefixFailure line 79
  22. def OAI.SharpTerminalLeave.UniformPrefixObligation line 83
  23. theorem OAI.SharpTerminalLeave.prefixDensity_bounds line 87
  24. theorem OAI.SharpTerminalLeave.step_card_mass_lower line 110
  25. theorem OAI.SharpTerminalLeave.evolve_card_mass_lower line 118
  26. theorem OAI.SharpTerminalLeave.mass_equality_prevents_early_stop line 130
  27. theorem OAI.SharpTerminalLeave.prefixM_mass line 142
  28. theorem OAI.SharpTerminalLeave.goodPrefix_mass line 150