OAI/Probability/Contingency/RepairVariance.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Repair Variance.

  1. theorem OAI.Contingency.variance_le_center line 15
  2. theorem OAI.Contingency.variance_repair_extension line 31
  3. abbrev OAI.Contingency.PaddedGraph.TransverseState line 86
  4. abbrev OAI.Contingency.PaddedGraph.DefectiveState line 88
  5. abbrev OAI.Contingency.PaddedGraph.GraphState line 91
  6. instance OAI.Contingency.PaddedGraph.transverseFinite line 94
  7. instance OAI.Contingency.PaddedGraph.defectiveFinite line 98
  8. instance OAI.Contingency.PaddedGraph.transverseFintype line 102
  9. instance OAI.Contingency.PaddedGraph.defectiveFintype line 104
  10. def OAI.Contingency.PaddedGraph.defectPair line 107
  11. theorem OAI.Contingency.PaddedGraph.defectPair_spec line 111
  12. theorem OAI.Contingency.PaddedGraph.defect_not_transversal line 116
  13. def OAI.Contingency.PaddedGraph.repairedState line 124
  14. theorem OAI.Contingency.PaddedGraph.coordinates_state_inverse line 129
  15. def OAI.Contingency.PaddedGraph.transverseTuple line 144
  16. theorem OAI.Contingency.PaddedGraph.tuple_transverseTuple line 148
  17. def OAI.Contingency.PaddedGraph.rootProfile line 161
  18. theorem OAI.Contingency.PaddedGraph.rootProfile_state line 165
  19. def OAI.Contingency.PaddedGraph.transverseProfile line 175
  20. theorem OAI.Contingency.PaddedGraph.transverseProfile_state line 179
  21. theorem OAI.Contingency.PaddedGraph.transverseProfile_injective line 185
  22. def OAI.Contingency.PaddedGraph.taggedRepair line 191
  23. theorem OAI.Contingency.PaddedGraph.taggedRepair_injective line 195
  24. theorem OAI.Contingency.PaddedGraph.defect_type_unique line 218
  25. theorem OAI.Contingency.PaddedGraph.stateCoordinates_box line 234
  26. theorem OAI.Contingency.PaddedGraph.fullOccupancy_state line 241
  27. theorem OAI.Contingency.PaddedGraph.stateCoordinates_transverse_vertex line 247
  28. theorem OAI.Contingency.PaddedGraph.stateCoordinates_defect_vertex line 255
  29. theorem OAI.Contingency.PaddedGraph.state_kernel_weight line 278
  30. def OAI.Contingency.PaddedGraph.repairEdge line 286
  31. theorem OAI.Contingency.PaddedGraph.stateCoordinates_inj_feasible line 290
  32. theorem OAI.Contingency.PaddedGraph.repairEdge_injective line 297
  33. def OAI.Contingency.PaddedGraph.fullRepairEdges line 307
  34. def OAI.Contingency.PaddedGraph.fullEdges line 314
  35. def OAI.Contingency.PaddedGraph.graphEnergy line 319
  36. theorem OAI.Contingency.PaddedGraph.graphEnergy_nonneg line 324
  37. theorem OAI.Contingency.PaddedGraph.unitEnergy_le_graphEnergy line 328
  38. theorem OAI.Contingency.PaddedGraph.repairEdge_energy line 336
  39. theorem OAI.Contingency.PaddedGraph.repairEnergy_le_graphEnergy line 352
  40. def OAI.Contingency.PaddedGraph.graphUnderlying line 376
  41. theorem OAI.Contingency.PaddedGraph.graphUnderlying_injective line 379
  42. def OAI.Contingency.PaddedGraph.graphVariance line 398
  43. theorem OAI.Contingency.PaddedGraph.graph_poincare_exact line 405
  44. theorem OAI.Contingency.PaddedGraph.poincare_constant_le line 453
  45. theorem OAI.Contingency.PaddedGraph.graph_poincare line 471
  46. def OAI.Contingency.PaddedGraph.graphCoordinates line 491
  47. theorem OAI.Contingency.PaddedGraph.graph_feasible line 494
  48. theorem OAI.Contingency.PaddedGraph.graphCoordinates_injective line 499
  49. def OAI.Contingency.PaddedGraph.GraphAdj line 504
  50. instance OAI.Contingency.PaddedGraph.graphAdjDecidable line 507
  51. theorem OAI.Contingency.PaddedGraph.GraphAdj.symm line 509
  52. theorem OAI.Contingency.PaddedGraph.GraphAdj.irrefl line 512
  53. def OAI.Contingency.PaddedGraph.unitCandidates line 529
  54. def OAI.Contingency.PaddedGraph.outgoing line 534
  55. def OAI.Contingency.PaddedGraph.incomingDefects line 538
  56. theorem OAI.Contingency.PaddedGraph.incoming_card line 542
  57. theorem OAI.Contingency.PaddedGraph.neighbors_cover line 556
  58. theorem OAI.Contingency.PaddedGraph.graph_degree line 589