OAI/Combinatorics/MatchingCount/Graphs/LabelOrder.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.NumberedHierarchy.labelOrder line 16
  2. def OAI.MatchingFPRAS.NumberedHierarchy.abstractTree line 28
  3. lemma OAI.MatchingFPRAS.NumberedHierarchy.abstractTree_acyclic line 32
  4. lemma OAI.MatchingFPRAS.NumberedHierarchy.abstractTree_adj line 36
  5. def OAI.MatchingFPRAS.NumberedHierarchy.tree line 45
  6. instance OAI.MatchingFPRAS.NumberedHierarchy.treeDec line 50
  7. lemma OAI.MatchingFPRAS.NumberedHierarchy.tree_adj line 54
  8. lemma OAI.MatchingFPRAS.NumberedHierarchy.tree_eq line 58
  9. lemma OAI.MatchingFPRAS.NumberedHierarchy.tree_acyclic line 62
  10. lemma OAI.MatchingFPRAS.NumberedHierarchy.bags_nonempty line 68
  11. lemma OAI.MatchingFPRAS.NumberedHierarchy.bags_adjacent line 73
  12. lemma OAI.MatchingFPRAS.NumberedHierarchy.bags_ranked line 95
  13. lemma OAI.MatchingFPRAS.NumberedHierarchy.height_step line 108
  14. def OAI.MatchingFPRAS.RationalSource.parent line 133
  15. def OAI.MatchingFPRAS.RationalSource.tree line 136
  16. lemma OAI.MatchingFPRAS.RationalSource.tree_acyclic line 139
  17. lemma OAI.MatchingFPRAS.RationalSource.parent_rank line 142
  18. lemma OAI.MatchingFPRAS.RationalSource.raw_cast line 147
  19. lemma OAI.MatchingFPRAS.RationalSource.realB_floor line 156
  20. lemma OAI.MatchingFPRAS.RationalSource.realB_upper line 160
  21. lemma OAI.MatchingFPRAS.RationalSource.realB_near line 168
  22. lemma OAI.MatchingFPRAS.RationalSource.bags_adjacent line 178
  23. lemma OAI.MatchingFPRAS.RationalSource.bags_ranked line 183
  24. lemma OAI.MatchingFPRAS.RationalSource.incident_exists line 189
  25. lemma OAI.MatchingFPRAS.RationalSource.bags_nonempty line 208
  26. def OAI.MatchingFPRAS.RationalSource.realLabel line 212
  27. lemma OAI.MatchingFPRAS.RationalSource.real_not_diag line 217
  28. def OAI.MatchingFPRAS.RationalSource.coloredReal line 225
  29. lemma OAI.MatchingFPRAS.RationalSource.coloredReal_injective line 232
  30. def OAI.MatchingFPRAS.RationalSource.realPortion line 237
  31. lemma OAI.MatchingFPRAS.RationalSource.realPortion_on line 240
  32. lemma OAI.MatchingFPRAS.RationalSource.realPortion_off line 244
  33. lemma OAI.MatchingFPRAS.RationalSource.pathActivity_pos line 250
  34. lemma OAI.MatchingFPRAS.RationalSource.pathActivity_le_realB line 264
  35. def OAI.MatchingFPRAS.RationalSource.bagHeight line 270
  36. lemma OAI.MatchingFPRAS.RationalSource.realPortion_nonneg line 272
  37. lemma OAI.MatchingFPRAS.RationalSource.realPortion_le_height line 280
  38. def OAI.MatchingFPRAS.RationalSource.bagWeight line 298
  39. lemma OAI.MatchingFPRAS.RationalSource.bagWeight_range line 301
  40. lemma OAI.MatchingFPRAS.RationalSource.bagHeight_one line 315
  41. lemma OAI.MatchingFPRAS.RationalSource.bagHeight_le line 318
  42. lemma OAI.MatchingFPRAS.RationalSource.bagHeight_step line 324
  43. lemma OAI.MatchingFPRAS.RationalSource.bagWeight_global line 329
  44. def OAI.MatchingFPRAS.RationalSource.sampler line 349
  45. theorem OAI.MatchingFPRAS.RationalSource.sampler_tv line 358
  46. lemma OAI.MatchingFPRAS.Transport.gibbs_instances line 388
  47. lemma OAI.MatchingFPRAS.Transport.slotLaw_of_weight line 394
  48. lemma OAI.MatchingFPRAS.Transport.top_marginal_tv line 402
  49. def OAI.MatchingFPRAS.Transport.rationalBase line 420
  50. lemma OAI.MatchingFPRAS.Transport.rationalBase_cast line 422
  51. lemma OAI.MatchingFPRAS.Transport.reaches_cast line 425
  52. def OAI.MatchingFPRAS.Transport.endpoint line 431
  53. lemma OAI.MatchingFPRAS.Transport.endpoint_eq line 437
  54. lemma OAI.MatchingFPRAS.Transport.endpoint_reaches line 451
  55. def OAI.MatchingFPRAS.RationalSource.topSampler line 473
  56. theorem OAI.MatchingFPRAS.RationalSource.topSampler_tv line 479