OAI/Probability/Contingency/LocalRepair.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Local Repair.

  1. def OAI.Contingency.PaddedGraph.inverseRepair line 17
  2. theorem OAI.Contingency.PaddedGraph.inverseRepair_repair line 22
  3. theorem OAI.Contingency.PaddedGraph.repair_inverseRepair line 33
  4. theorem OAI.Contingency.PaddedGraph.inverseRepair_defect line 43
  5. def OAI.Contingency.PaddedGraph.slotList line 48
  6. theorem OAI.Contingency.PaddedGraph.mem_slotList line 51
  7. theorem OAI.Contingency.PaddedGraph.length_slotList line 55
  8. def OAI.Contingency.PaddedGraph.typeList line 58
  9. theorem OAI.Contingency.PaddedGraph.mem_typeList line 61
  10. theorem OAI.Contingency.PaddedGraph.length_typeList line 64
  11. instance OAI.Contingency.PaddedGraph.feasibleDecidable line 67
  12. instance OAI.Contingency.PaddedGraph.transversalDecidable line 70
  13. instance OAI.Contingency.PaddedGraph.defectAtDecidable line 73
  14. def OAI.Contingency.PaddedGraph.inverseNeighbors line 79
  15. theorem OAI.Contingency.PaddedGraph.length_inverseNeighbors line 87
  16. theorem OAI.Contingency.PaddedGraph.repairedState_eq line 97
  17. theorem OAI.Contingency.PaddedGraph.mem_inverseNeighbors line 106
  18. def OAI.Contingency.PaddedGraph.smallList line 155
  19. theorem OAI.Contingency.PaddedGraph.mem_smallList line 158
  20. theorem OAI.Contingency.PaddedGraph.length_smallList line 162
  21. def OAI.Contingency.PaddedGraph.coordList line 167
  22. theorem OAI.Contingency.PaddedGraph.mem_coordList line 169
  23. theorem OAI.Contingency.PaddedGraph.length_coordList line 172
  24. def OAI.Contingency.PaddedGraph.allowedState line 179
  25. instance OAI.Contingency.PaddedGraph.allowedStateDecidable line 182
  26. theorem OAI.Contingency.PaddedGraph.graph_allowed line 185
  27. def OAI.Contingency.PaddedGraph.localExchange line 192
  28. theorem OAI.Contingency.PaddedGraph.localExchange_eq line 199
  29. theorem OAI.Contingency.PaddedGraph.localExchange_coordinates line 203
  30. def OAI.Contingency.PaddedGraph.unitNeighbors line 208
  31. theorem OAI.Contingency.PaddedGraph.length_unitNeighbors line 213
  32. theorem OAI.Contingency.PaddedGraph.unitNeighbors_allowed line 225
  33. theorem OAI.Contingency.PaddedGraph.graph_vertex line 230
  34. theorem OAI.Contingency.PaddedGraph.unitEdge_of_exchange line 235
  35. theorem OAI.Contingency.PaddedGraph.mem_unitNeighbors line 249
  36. def OAI.Contingency.PaddedGraph.localRepair line 294
  37. theorem OAI.Contingency.PaddedGraph.localRepair_eq line 299
  38. def OAI.Contingency.PaddedGraph.findDefect line 303
  39. theorem OAI.Contingency.PaddedGraph.findDefect_some line 306
  40. theorem OAI.Contingency.PaddedGraph.findDefect_none line 311
  41. theorem OAI.Contingency.PaddedGraph.findDefect_transverse line 316
  42. theorem OAI.Contingency.PaddedGraph.findDefect_defective line 321
  43. def OAI.Contingency.PaddedGraph.localOutgoing line 332
  44. theorem OAI.Contingency.PaddedGraph.length_localOutgoing line 337
  45. theorem OAI.Contingency.PaddedGraph.localOutgoing_transverse line 341
  46. theorem OAI.Contingency.PaddedGraph.localOutgoing_defective line 344
  47. theorem OAI.Contingency.PaddedGraph.mem_localOutgoing line 348
  48. theorem OAI.Contingency.PaddedGraph.repairAdj_iff line 360
  49. def OAI.Contingency.PaddedGraph.localNeighbors line 391
  50. theorem OAI.Contingency.PaddedGraph.localNeighbors_nodup line 394
  51. theorem OAI.Contingency.PaddedGraph.length_localNeighbors line 397
  52. theorem OAI.Contingency.PaddedGraph.mem_localNeighbors line 409
  53. theorem OAI.Contingency.PaddedGraph.localNeighbors_allowed line 417
  54. def OAI.Contingency.IntegerDraw.unitWeights line 448
  55. theorem OAI.Contingency.IntegerDraw.unitWeights_total line 450
  56. theorem OAI.Contingency.IntegerDraw.unitWeights_weight line 457
  57. def OAI.Contingency.PaddedGraph.graphStateOf line 467
  58. theorem OAI.Contingency.PaddedGraph.graphStateOf_underlying line 470
  59. def OAI.Contingency.PaddedGraph.graphNeighborList line 476
  60. theorem OAI.Contingency.PaddedGraph.graphNeighborList_nodup line 480
  61. theorem OAI.Contingency.PaddedGraph.mem_graphNeighborList line 487
  62. theorem OAI.Contingency.PaddedGraph.graphNeighborList_length line 501
  63. theorem OAI.Contingency.PaddedGraph.graphNeighborList_card line 506
  64. def OAI.Contingency.PaddedGraph.selectLocalNeighbor line 515
  65. def OAI.Contingency.PaddedGraph.localProposal line 518
  66. theorem OAI.Contingency.PaddedGraph.localProposal_actual line 523
  67. theorem OAI.Contingency.PaddedGraph.localProposal_count_offdiag line 526
  68. theorem OAI.Contingency.PaddedGraph.localProposal_toLaw line 545