OAI/Probability/Contingency/Completions.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Completions.

  1. def OAI.Contingency.PaddedGraph.rowPadding line 16
  2. def OAI.Contingency.PaddedGraph.colPadding line 19
  3. def OAI.Contingency.PaddedGraph.Completion line 24
  4. instance OAI.Contingency.PaddedGraph.completionFinite line 30
  5. def OAI.Contingency.PaddedGraph.completionRepair line 49
  6. theorem OAI.Contingency.PaddedGraph.completionRepair_injective line 94
  7. def OAI.Contingency.PaddedGraph.weight line 105
  8. theorem OAI.Contingency.PaddedGraph.weight_repair_le line 109
  9. theorem OAI.Contingency.PaddedGraph.joint_repair_injective line 120
  10. instance OAI.Contingency.PaddedGraph.feasibleFinite line 148
  11. def OAI.Contingency.PaddedGraph.Prefix line 175
  12. def OAI.Contingency.PaddedGraph.ChildStates line 178
  13. def OAI.Contingency.PaddedGraph.DefectStates line 183
  14. instance OAI.Contingency.PaddedGraph.(instance at line 188) line 188
  15. instance OAI.Contingency.PaddedGraph.(instance at line 191) line 191
  16. def OAI.Contingency.PaddedGraph.conditionalRepair line 195
  17. def OAI.Contingency.PaddedGraph.childFiber line 208
  18. def OAI.Contingency.PaddedGraph.defectFiber line 212
  19. instance OAI.Contingency.PaddedGraph.(instance at line 216) line 216
  20. instance OAI.Contingency.PaddedGraph.(instance at line 219) line 219
  21. def OAI.Contingency.PaddedGraph.conditionalCompletionRepair line 223
  22. theorem OAI.Contingency.PaddedGraph.conditionalCompletionRepair_injective line 229
  23. def OAI.Contingency.PaddedGraph.childMass line 243
  24. def OAI.Contingency.PaddedGraph.defectMass line 247
  25. theorem OAI.Contingency.PaddedGraph.conditional_repair_bound line 253
  26. theorem OAI.Contingency.PaddedGraph.conditional_repair_max line 262
  27. theorem OAI.Contingency.softPenalty_zero_iff line 282
  28. def OAI.Contingency.PaddedGraph.smallSet line 299
  29. def OAI.Contingency.PaddedGraph.capacity line 302
  30. def OAI.Contingency.PaddedGraph.paddedRow line 305
  31. def OAI.Contingency.PaddedGraph.paddedCol line 308
  32. def OAI.Contingency.PaddedGraph.fullCoordinates line 313
  33. theorem OAI.Contingency.PaddedGraph.fullCoordinates_x line 317
  34. theorem OAI.Contingency.PaddedGraph.fullCoordinates_q line 321
  35. theorem OAI.Contingency.PaddedGraph.completion_cell_le line 326
  36. theorem OAI.Contingency.PaddedGraph.fullCoordinates_inBox line 336
  37. theorem OAI.Contingency.PaddedGraph.fullCoordinates_penalty_zero line 350
  38. theorem OAI.Contingency.PaddedGraph.sum_rowSum line 385
  39. theorem OAI.Contingency.PaddedGraph.sum_colSum line 388
  40. theorem OAI.Contingency.PaddedGraph.padding_totals line 392
  41. theorem OAI.Contingency.PaddedGraph.completion_small_totals line 396
  42. theorem OAI.Contingency.PaddedGraph.fullCoordinates_total line 406
  43. theorem OAI.Contingency.PaddedGraph.completion_softWeight_one line 426
  44. def OAI.Contingency.PaddedGraph.LargeChoices line 437
  45. instance OAI.Contingency.PaddedGraph.(instance at line 440) line 440
  46. instance OAI.Contingency.PaddedGraph.(instance at line 452) line 452
  47. def OAI.Contingency.PaddedGraph.CompletionEquations line 455
  48. def OAI.Contingency.PaddedGraph.choiceCompletion line 460
  49. def OAI.Contingency.PaddedGraph.completionChoice line 465
  50. def OAI.Contingency.PaddedGraph.completionChoiceEquiv line 472
  51. theorem OAI.Contingency.PaddedGraph.choice_softWeight line 480
  52. theorem OAI.Contingency.PaddedGraph.sum_choice_softWeight line 508