OAI/Computability/BinPacking/PCP/PreprocessingLazyWords.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.Overlay.originalPortGraph line 20
2. def OAI.BinPackingGames.Foundations.PCP.Overlay.rotate line 24
3. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.rotate_involutive line 29
4. def OAI.BinPackingGames.Foundations.PCP.Overlay.portGraph line 38
5. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.portGraph_rot_inl line 46
6. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.portGraph_rot_inr line 51
7. def OAI.BinPackingGames.Foundations.PCP.Overlay.constraintGraph line 56
8. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.constraintGraph_tail line 70
9. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.constraintGraph_portGraph line 73
10. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.edgeSatisfied_inl line 77
11. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.edgeSatisfied_inr line 87
12. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.complete line 91
13. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.satisfiable_iff line 101
14. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.rejectionCount_eq line 113
15. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.card_ports line 122
16. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.card_darts line 125
17. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.operator_mix line 134
18. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.energy_convex_mix line 153
19. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.energy_bound line 168
20. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.energy_bound_three_quarters line 203
21. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.spectralCertificate_seven_eighths line 222
22. theorem OAI.BinPackingGames.Foundations.PCP.Overlay.constraintGraph_spectralCertificate line 235
23. def OAI.BinPackingGames.Foundations.PCP.LazyConstraint.constraintGraph line 255
24. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.constraintGraph_tail line 267
25. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.constraintGraph_reverse line 270
26. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.constraintGraph_portGraph line 273
27. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.edgeSatisfied_false line 277
28. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.edgeSatisfied_true line 281
29. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.complete line 290
30. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.complete_iff line 300
31. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.satisfiable_iff line 311
32. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.rejectionCount_eq line 319
33. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.card_ports line 328
34. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.card_darts line 332
35. theorem OAI.BinPackingGames.Foundations.PCP.LazyConstraint.rejection_density_eq_half line 336
36. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts line 352
37. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inl_val line 354
38. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlayPorts_inr_val line 357
39. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts line 360
40. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_false_val line 363
41. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazyPorts_true_val line 367
42. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.materialize line 371
43. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize line 385
44. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.rotation_materialize_image line 396
45. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.accepts_materialize line 403
46. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.constraintGraph_ext line 410
47. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.baseGraph_materialize line 424
48. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlay line 440
49. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_old line 445
50. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlay_rotation_expander line 452
51. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_old line 459
52. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlay_accepts_expander line 466
53. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.overlay_semantics line 472
54. def OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazy line 480
55. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_false line 483
56. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazy_rotation_true line 489
57. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_false line 496
58. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazy_accepts_true line 502
59. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingOverlayTables.lazy_semantics line 509
60. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.row line 524
61. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.trueRelation line 528
62. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.stayRow line 530
63. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.moveRow line 533
64. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.reverseMap line 539
65. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.relation_ext line 541
66. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_stay line 548
67. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.row_lazy_move line 561
68. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.stayRow_reverse_val line 574
69. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.moveRow_reverse_val line 579
70. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.relationWords_true line 587
71. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.stayRow_words line 591
72. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.moveRow_words line 597
73. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.ofFn_rowIndex line 604
74. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.flatRows_list line 618
75. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.ofFn_lazyPorts line 625
76. def OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.vertexRows line 638
77. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_length line 642
78. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.flatRows_lazy line 647
79. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.vertexRows_words line 657
80. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.tableWords_lazy line 677
81. theorem OAI.BinPackingGames.Foundations.PCP.PreprocessingLazyWords.tableBits_lazy line 682