OAI/Combinatorics/MatchingEntropy/TriangleExpansion.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.Refined.CubicColoring line 17
  2. def OAI.MatchingEntropyBounds.Refined.colorEdges line 20
  3. def OAI.MatchingEntropyBounds.Refined.triangleTip line 22

    Also declared: ComparatorChallenges/TriangleFace.lean:90 (same declaration text).

  4. def OAI.MatchingEntropyBounds.Refined.triangleCollapse line 24

    Also declared: ComparatorChallenges/TriangleFace.lean:92 (same declaration text).

  5. def OAI.MatchingEntropyBounds.Refined.reattach line 26

    Also declared: ComparatorChallenges/TriangleFace.lean:94 (same declaration text).

  6. theorem OAI.MatchingEntropyBounds.Refined.collapse_reattach line 30

    Also declared: ComparatorChallenges/TriangleFace.lean:98 (same declaration text).

  7. def OAI.MatchingEntropyBounds.Refined.triangleExpansion line 37

    Also declared: ComparatorChallenges/TriangleFace.lean:105 (same declaration text).

  8. def OAI.MatchingEntropyBounds.Refined.expandedColor line 49
  9. def OAI.MatchingEntropyBounds.Refined.triangleVertices line 51

    Also declared: ComparatorChallenges/TriangleFace.lean:117 (same declaration text).

  10. def OAI.MatchingEntropyBounds.Refined.vertexColorEdge line 53
  11. def OAI.MatchingEntropyBounds.Refined.triangleExtension line 56
  12. def OAI.MatchingEntropyBounds.Refined.IsSimpleLabelled line 62
  13. def OAI.MatchingEntropyBounds.Refined.KleeV line 68
  14. def OAI.MatchingEntropyBounds.Refined.KleeE line 72
  15. instance OAI.MatchingEntropyBounds.Refined.kleeVFintype line 76
  16. instance OAI.MatchingEntropyBounds.Refined.kleeEFintype line 82
  17. instance OAI.MatchingEntropyBounds.Refined.kleeVDecEq line 88
  18. instance OAI.MatchingEntropyBounds.Refined.kleeEDecEq line 89
  19. def OAI.MatchingEntropyBounds.Refined.kleeRoot line 91
  20. def OAI.MatchingEntropyBounds.Refined.kleeColor line 95
  21. def OAI.MatchingEntropyBounds.Refined.kleeGraph line 99
  22. def OAI.MatchingEntropyBounds.Refined.kleeUniform line 103
  23. def OAI.MatchingEntropyBounds.Refined.coloredVector line 105
  24. def OAI.MatchingEntropyBounds.Refined.kleeTriangle line 108
  25. def OAI.MatchingEntropyBounds.Refined.kleeLaw line 111
  26. theorem OAI.MatchingEntropyBounds.Refined.triangleTip_injective line 118
  27. theorem OAI.MatchingEntropyBounds.Refined.reattach_eq_tip line 123
  28. theorem OAI.MatchingEntropyBounds.Refined.reattach_eq_inl line 130
  29. theorem OAI.MatchingEntropyBounds.Refined.expanded_incident_old_tip line 138
  30. theorem OAI.MatchingEntropyBounds.Refined.expanded_incident_old_inl line 146
  31. theorem OAI.MatchingEntropyBounds.Refined.expanded_incident_new_tip line 152
  32. theorem OAI.MatchingEntropyBounds.Refined.expanded_incident_new_inl line 160
  33. theorem OAI.MatchingEntropyBounds.Refined.vertexColorEdge_spec line 166
  34. theorem OAI.MatchingEntropyBounds.Refined.eq_vertexColorEdge line 172
  35. theorem OAI.MatchingEntropyBounds.Refined.colorEdges_matching line 177
  36. def OAI.MatchingEntropyBounds.Refined.colorMatching line 186
  37. theorem OAI.MatchingEntropyBounds.Refined.cubicColoring_expansion line 190
  38. theorem OAI.MatchingEntropyBounds.Refined.triangleVertices_eq line 224
  39. theorem OAI.MatchingEntropyBounds.Refined.mem_triangleVertices_tip line 229
  40. theorem OAI.MatchingEntropyBounds.Refined.reattach_mem_triangle line 233
  41. theorem OAI.MatchingEntropyBounds.Refined.expanded_crosses_old line 240
  42. theorem OAI.MatchingEntropyBounds.Refined.expanded_crosses_new line 252
  43. theorem OAI.MatchingEntropyBounds.Refined.triangleVertices_odd line 257
  44. theorem OAI.MatchingEntropyBounds.Refined.expanded_cutMass line 265
  45. def OAI.MatchingEntropyBounds.Refined.incidentChoice line 272
  46. theorem OAI.MatchingEntropyBounds.Refined.incidentChoice_spec line 276
  47. theorem OAI.MatchingEntropyBounds.Refined.eq_incidentChoice line 281
  48. def OAI.MatchingEntropyBounds.Refined.expandEdges line 286
  49. theorem OAI.MatchingEntropyBounds.Refined.expandEdges_matching line 290
  50. def OAI.MatchingEntropyBounds.Refined.expandMatching line 333
  51. theorem OAI.MatchingEntropyBounds.Refined.expandMatching_injective line 337
  52. theorem OAI.MatchingEntropyBounds.Refined.expandMatching_indicator line 346
  53. def OAI.MatchingEntropyBounds.Refined.CrossOnce line 364
  54. theorem OAI.MatchingEntropyBounds.Refined.cutMass_indicator_card line 369
  55. theorem OAI.MatchingEntropyBounds.Refined.crossOnce_of_cut_eq_one line 377
  56. def OAI.MatchingEntropyBounds.Refined.contractEdges line 397
  57. theorem OAI.MatchingEntropyBounds.Refined.contractEdges_matching line 402
  58. def OAI.MatchingEntropyBounds.Refined.contractMatching line 419
  59. theorem OAI.MatchingEntropyBounds.Refined.fin3_add_one_ne line 424
  60. theorem OAI.MatchingEntropyBounds.Refined.expand_contract line 427
  61. theorem OAI.MatchingEntropyBounds.Refined.range_expandMatching_of_crossOnce line 458
  62. theorem OAI.MatchingEntropyBounds.Refined.cutMass_mean line 463
  63. theorem OAI.MatchingEntropyBounds.Refined.positive_law_tight_cut line 469
  64. theorem OAI.MatchingEntropyBounds.Refined.expanded_push_mean line 482
  65. theorem OAI.MatchingEntropyBounds.Refined.triangleExtension_injective line 492
  66. theorem OAI.MatchingEntropyBounds.Refined.expanded_push_feasible line 499
  67. theorem OAI.MatchingEntropyBounds.Refined.expanded_pull_simplex line 506
  68. theorem OAI.MatchingEntropyBounds.Refined.expanded_pull_feasible line 522
  69. theorem OAI.MatchingEntropyBounds.Refined.expansion_image_eq line 536
  70. theorem OAI.MatchingEntropyBounds.Refined.expansion_image_extreme line 557
  71. theorem OAI.MatchingEntropyBounds.Refined.expansion_entropy line 576
  72. theorem OAI.MatchingEntropyBounds.Refined.expansion_face line 590
  73. theorem OAI.MatchingEntropyBounds.Refined.simplicity_expansion line 608
  74. theorem OAI.MatchingEntropyBounds.Refined.klee_cubic line 636
  75. theorem OAI.MatchingEntropyBounds.Refined.klee_cardV line 646
  76. theorem OAI.MatchingEntropyBounds.Refined.klee_cardE line 654
  77. theorem OAI.MatchingEntropyBounds.Refined.klee_simple_one line 662
  78. theorem OAI.MatchingEntropyBounds.Refined.klee_simple line 674
  79. theorem OAI.MatchingEntropyBounds.Refined.klee_graph_properties line 682