OAI/Combinatorics/MatchingCount/Sampling/PM.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatchingFPRAS.Transport.PM line 14
  2. structure OAI.MatchingFPRAS.Transport.RawDemand line 16
  3. structure OAI.MatchingFPRAS.Transport.DemandEncoding line 23
  4. abbrev OAI.MatchingFPRAS.Transport.DemandTag line 36
  5. def OAI.MatchingFPRAS.Transport.padOccurrences line 38
  6. lemma OAI.MatchingFPRAS.Transport.padOccurrences_recovers line 42
  7. lemma OAI.MatchingFPRAS.Transport.tag_card line 55
  8. lemma OAI.MatchingFPRAS.Transport.tag_card_bound line 62
  9. def OAI.MatchingFPRAS.Transport.DemandEncoding.code line 79
  10. theorem OAI.MatchingFPRAS.Transport.DemandEncoding.code_recovers line 83
  11. def OAI.MatchingFPRAS.Transport.DemandEncoding.tag line 103
  12. def OAI.MatchingFPRAS.Transport.DemandEncoding.finiteCode line 107
  13. theorem OAI.MatchingFPRAS.Transport.DemandEncoding.finiteCode_recovers line 110
  14. theorem OAI.MatchingFPRAS.Transport.DemandEncoding.code_injective line 120
  15. structure OAI.MatchingFPRAS.Transport.EmbeddedCell line 136
  16. def OAI.MatchingFPRAS.Transport.EmbeddedCell.outsideFirst line 150
  17. def OAI.MatchingFPRAS.Transport.EmbeddedCell.outsideSecond line 152
  18. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.outsideFirst_matching line 154
  19. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.outsideSecond_matching line 157
  20. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.context_vertices_disjoint line 160
  21. def OAI.MatchingFPRAS.Transport.EmbeddedCell.attachFirst line 163
  22. def OAI.MatchingFPRAS.Transport.EmbeddedCell.attachSecond line 168
  23. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.attachFirst_val line 174
  24. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.attachSecond_val line 179
  25. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.source_first_val line 184
  26. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.source_second_val line 192
  27. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.attach_outside line 200
  28. def OAI.MatchingFPRAS.Transport.EmbeddedCell.encode line 224
  29. def OAI.MatchingFPRAS.Transport.EmbeddedCell.switchEncoding line 250
  30. def OAI.MatchingFPRAS.Transport.EmbeddedCell.errorZeroEncoding line 259
  31. def OAI.MatchingFPRAS.Transport.EmbeddedCell.errorOneEncoding line 268
  32. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.zero_guide_contains line 279
  33. lemma OAI.MatchingFPRAS.Transport.EmbeddedCell.one_guide_contains line 286
  34. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.rawDemand line 308
  35. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.embeddedPair line 311
  36. def OAI.MatchingFPRAS.Transport.matchingWeight line 356
  37. lemma OAI.MatchingFPRAS.Transport.matchingWeight_pos line 358
  38. def OAI.MatchingFPRAS.Transport.partition line 363
  39. lemma OAI.MatchingFPRAS.Transport.partition_pos line 367
  40. def OAI.MatchingFPRAS.Transport.gibbs line 373
  41. lemma OAI.MatchingFPRAS.Transport.gibbs_pos line 376
  42. lemma OAI.MatchingFPRAS.Transport.gibbs_sum line 379