OAI/Combinatorics/MatchingCount/Sampling/Corner.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.CellPaths.corner line 13
  2. def OAI.MatchingFPRAS.Transport.CellPaths.vertices line 15
  3. lemma OAI.MatchingFPRAS.Transport.CellPaths.ends_eq line 20
  4. lemma OAI.MatchingFPRAS.Transport.CellPaths.inside_disjoint_span line 24
  5. lemma OAI.MatchingFPRAS.Transport.CellPaths.opposite_ends_even line 31
  6. lemma OAI.MatchingFPRAS.Transport.CellPaths.opposite_ends_odd line 41
  7. lemma OAI.MatchingFPRAS.Transport.CellPaths.opposite_span_even line 51
  8. lemma OAI.MatchingFPRAS.Transport.CellPaths.opposite_span_odd line 60
  9. lemma OAI.MatchingFPRAS.Transport.CellPaths.even_blocks_union line 69
  10. lemma OAI.MatchingFPRAS.Transport.CellPaths.odd_blocks_union line 79
  11. def OAI.MatchingFPRAS.Transport.CellPaths.assemble line 88
  12. lemma OAI.MatchingFPRAS.Transport.CellPaths.matching_even_full line 90
  13. lemma OAI.MatchingFPRAS.Transport.CellPaths.matching_odd_full line 107
  14. def OAI.MatchingFPRAS.Transport.CellPaths.sideBit line 125
  15. def OAI.MatchingFPRAS.Transport.CellPaths.blocks line 127
  16. def OAI.MatchingFPRAS.Transport.CellPaths.pieces line 130
  17. lemma OAI.MatchingFPRAS.Transport.CellPaths.same_bit_spans line 134
  18. lemma OAI.MatchingFPRAS.Transport.CellPaths.blocks_disjoint line 145
  19. lemma OAI.MatchingFPRAS.Transport.CellPaths.assembled_matching line 157
  20. lemma OAI.MatchingFPRAS.Transport.CellPaths.assemble_val line 172
  21. lemma OAI.MatchingFPRAS.Transport.CellPaths.pieces_matching line 187
  22. def OAI.MatchingFPRAS.Transport.CellPaths.orientationPieces line 196
  23. def OAI.MatchingFPRAS.Transport.CellPaths.switchPieces line 199
  24. def OAI.MatchingFPRAS.Transport.CellPaths.repairPieces line 202
  25. def OAI.MatchingFPRAS.Transport.CellPaths.guidePieces line 205
  26. def OAI.MatchingFPRAS.Transport.CellPaths.Repairs line 208
  27. lemma OAI.MatchingFPRAS.Transport.CellPaths.orientation_pieces_matching line 212
  28. lemma OAI.MatchingFPRAS.Transport.CellPaths.switch_pieces_matching line 217
  29. lemma OAI.MatchingFPRAS.Transport.CellPaths.repair_pieces_matching line 222
  30. lemma OAI.MatchingFPRAS.Transport.CellPaths.guide_pieces_matching line 227
  31. def OAI.MatchingFPRAS.Transport.CellPaths.orientation line 232
  32. def OAI.MatchingFPRAS.Transport.CellPaths.switched line 234
  33. def OAI.MatchingFPRAS.Transport.CellPaths.repaired line 236
  34. def OAI.MatchingFPRAS.Transport.CellPaths.guide line 238
  35. lemma OAI.MatchingFPRAS.Transport.CellPaths.orientation_matching line 240
  36. lemma OAI.MatchingFPRAS.Transport.CellPaths.switched_matching line 243
  37. lemma OAI.MatchingFPRAS.Transport.CellPaths.repaired_matching line 246
  38. lemma OAI.MatchingFPRAS.Transport.CellPaths.guide_matching line 250
  39. lemma OAI.MatchingFPRAS.Transport.CellPaths.component_subset_assemble line 254
  40. lemma OAI.MatchingFPRAS.Transport.CellPaths.closed_subset_guide line 262
  41. def OAI.MatchingFPRAS.Transport.CellPaths.drops line 267
  42. def OAI.MatchingFPRAS.Transport.CellPaths.additions line 270
  43. lemma OAI.MatchingFPRAS.Transport.CellPaths.orientation_val line 274
  44. lemma OAI.MatchingFPRAS.Transport.CellPaths.switched_val line 278
  45. lemma OAI.MatchingFPRAS.Transport.CellPaths.repaired_val line 282
  46. lemma OAI.MatchingFPRAS.Transport.CellPaths.guide_val line 287
  47. lemma OAI.MatchingFPRAS.Transport.CellPaths.two_orientation_pieces line 292
  48. lemma OAI.MatchingFPRAS.Transport.CellPaths.switch_piece_val line 297
  49. lemma OAI.MatchingFPRAS.Transport.CellPaths.repair_piece_conservation line 305
  50. lemma OAI.MatchingFPRAS.Transport.CellPaths.switch_conservation line 316
  51. lemma OAI.MatchingFPRAS.Transport.CellPaths.guide_piece_conservation line 333
  52. lemma OAI.MatchingFPRAS.Transport.CellPaths.guide_conservation line 351
  53. lemma OAI.MatchingFPRAS.Transport.CellPaths.boundary_card_eq line 364
  54. lemma OAI.MatchingFPRAS.Transport.CellPaths.additions_card line 370
  55. lemma OAI.MatchingFPRAS.Transport.CellPaths.modification_cards line 382
  56. lemma OAI.MatchingFPRAS.Transport.CellPaths.through_subset_orientation line 401
  57. lemma OAI.MatchingFPRAS.Transport.CellPaths.span_subset_vertices line 407
  58. def OAI.MatchingFPRAS.Transport.CellPaths.contextOne line 413
  59. def OAI.MatchingFPRAS.Transport.CellPaths.guideOne line 416
  60. lemma OAI.MatchingFPRAS.Transport.CellPaths.context_one_properties line 419
  61. lemma OAI.MatchingFPRAS.Transport.CellPaths.closed_subset_guide_one line 430
  62. lemma OAI.MatchingFPRAS.Transport.CellPaths.context_one_conservation line 441
  63. lemma OAI.MatchingFPRAS.Transport.CellPaths.switch_weight_bound line 448
  64. lemma OAI.MatchingFPRAS.Transport.CellPaths.guide_weight_bound line 461
  65. lemma OAI.MatchingFPRAS.Transport.CellPaths.context_one_weight_bound line 474