OAI/Combinatorics/MatchingCount/Sampling/Endpoints.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.GraphBridge.endpoints line 13
  2. def OAI.MatchingFPRAS.GraphBridge.selectedEdges line 15
  3. lemma OAI.MatchingFPRAS.GraphBridge.mem_selected line 18
  4. lemma OAI.MatchingFPRAS.GraphBridge.selected_increasing line 21
  5. def OAI.MatchingFPRAS.GraphBridge.edgeSelection line 27
  6. lemma OAI.MatchingFPRAS.GraphBridge.edgeSelection_selected line 29
  7. lemma OAI.MatchingFPRAS.GraphBridge.selected_edgeSelection line 35
  8. lemma OAI.MatchingFPRAS.GraphBridge.logical_iff_perfect line 47
  9. def OAI.MatchingFPRAS.GraphBridge.perfectEquiv line 68
  10. lemma OAI.MatchingFPRAS.GraphBridge.selected_prod line 77
  11. theorem OAI.MatchingFPRAS.GraphBridge.weighted_partition line 83
  12. def OAI.MatchingFPRAS.GraphBridge.rawActivity line 99
  13. lemma OAI.MatchingFPRAS.GraphBridge.rawActivity_pos line 102
  14. lemma OAI.MatchingFPRAS.GraphBridge.rawActivity_symm line 107
  15. theorem OAI.MatchingFPRAS.GraphBridge.raw_partition line 110
  16. theorem OAI.MatchingFPRAS.GraphBridge.complete_count line 123
  17. def OAI.MatchingFPRAS.Trial.cooling line 137
  18. lemma OAI.MatchingFPRAS.Trial.cooling_pos line 139
  19. lemma OAI.MatchingFPRAS.Trial.cooling_le_one line 141
  20. def OAI.MatchingFPRAS.Trial.raw line 147
  21. lemma OAI.MatchingFPRAS.Trial.raw_pos line 150
  22. lemma OAI.MatchingFPRAS.Trial.raw_le_one line 153
  23. lemma OAI.MatchingFPRAS.Trial.raw_cooling line 159
  24. lemma OAI.MatchingFPRAS.Trial.raw_zero line 170
  25. lemma OAI.MatchingFPRAS.Trial.raw_partition_pos line 174
  26. structure OAI.MatchingFPRAS.Trial.ScaleState line 178
  27. def OAI.MatchingFPRAS.Trial.ScaleState.activity line 185
  28. def OAI.MatchingFPRAS.Trial.ScaleState.nextActivity line 188
  29. lemma OAI.MatchingFPRAS.Trial.ScaleState.activity_pos line 191
  30. lemma OAI.MatchingFPRAS.Trial.ScaleState.nextActivity_pos line 194
  31. lemma OAI.MatchingFPRAS.Trial.ScaleState.cooling line 197
  32. lemma OAI.MatchingFPRAS.Trial.ScaleState.activity_bound line 205
  33. lemma OAI.MatchingFPRAS.Trial.ScaleState.cap line 212
  34. lemma OAI.MatchingFPRAS.Trial.ScaleState.partition_pos line 218
  35. lemma OAI.MatchingFPRAS.Trial.ScaleState.ratio line 222
  36. def OAI.MatchingFPRAS.Trial.initialScaleState line 231
  37. def OAI.MatchingFPRAS.Trial.ScaleState.Balanced line 242
  38. lemma OAI.MatchingFPRAS.Trial.initial_balanced line 246
  39. def OAI.MatchingFPRAS.Trial.ScaleState.matrix line 260
  40. lemma OAI.MatchingFPRAS.Trial.ScaleState.matrix_bounds line 265
  41. def OAI.MatchingFPRAS.Trial.ScaleState.updateVector line 272
  42. lemma OAI.MatchingFPRAS.Trial.ScaleState.updateVector_bounds line 276
  43. def OAI.MatchingFPRAS.Trial.ScaleState.update line 284
  44. lemma OAI.MatchingFPRAS.Trial.ScaleState.update_activity line 293
  45. def OAI.MatchingFPRAS.Trial.ScaleState.ratioEstimate line 300
  46. lemma OAI.MatchingFPRAS.Trial.ScaleState.ratioEstimate_nonneg line 304
  47. def OAI.MatchingFPRAS.Trial.stageData line 317
  48. theorem OAI.MatchingFPRAS.Trial.successful_update line 336
  49. theorem OAI.MatchingFPRAS.Counting.stage_product_error line 359
  50. def OAI.MatchingFPRAS.Counting.productEstimate line 403
  51. lemma OAI.MatchingFPRAS.Counting.positive_telescope line 408