OAI/Probability/Contingency/ResidualMargins.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Residual Margins.

  1. def OAI.Contingency.PaddedGraph.residualRow line 16
  2. def OAI.Contingency.PaddedGraph.residualCol line 17
  3. theorem OAI.Contingency.PaddedGraph.residualRow_nonneg line 19
  4. theorem OAI.Contingency.PaddedGraph.residualCol_nonneg line 25
  5. theorem OAI.Contingency.PaddedGraph.residualRow_zero line 31
  6. theorem OAI.Contingency.PaddedGraph.residualCol_zero line 36
  7. theorem OAI.Contingency.PaddedGraph.graph_small_totals line 41
  8. theorem OAI.Contingency.PaddedGraph.residual_totals line 51
  9. def OAI.Contingency.PaddedGraph.rowNat line 64
  10. def OAI.Contingency.PaddedGraph.colNat line 65
  11. theorem OAI.Contingency.PaddedGraph.rowNat_cast line 67
  12. theorem OAI.Contingency.PaddedGraph.colNat_cast line 69
  13. def OAI.Contingency.PaddedGraph.completionTable line 72
  14. def OAI.Contingency.PaddedGraph.tableCompletion line 86
  15. def OAI.Contingency.PaddedGraph.completionTableEquiv line 115
  16. theorem OAI.Contingency.PaddedGraph.completion_nonempty line 124
  17. theorem OAI.Contingency.PaddedGraph.graph_weight_pos line 136
  18. def OAI.Contingency.PaddedGraph.shiftCoord line 154
  19. theorem OAI.Contingency.PaddedGraph.shift_x line 157
  20. theorem OAI.Contingency.PaddedGraph.shift_q line 166
  21. theorem OAI.Contingency.PaddedGraph.shift_row line 176
  22. theorem OAI.Contingency.PaddedGraph.shift_col line 187
  23. theorem OAI.Contingency.PaddedGraph.unit_margin_movement line 198
  24. theorem OAI.Contingency.PaddedGraph.repair_margin_movement line 230
  25. theorem OAI.Contingency.PaddedGraph.graph_margin_movement line 244
  26. theorem OAI.Contingency.PaddedGraph.pattern_graphState line 275
  27. theorem OAI.Contingency.PaddedGraph.positive_vertex line 316
  28. theorem OAI.Contingency.PaddedGraph.positive_edge line 323
  29. def OAI.Contingency.tableInt line 361
  30. theorem OAI.Contingency.tableInt_row line 364
  31. theorem OAI.Contingency.tableInt_col line 368
  32. def OAI.Contingency.switchDirection line 373
  33. theorem OAI.Contingency.switchDirection_row line 376
  34. theorem OAI.Contingency.switchDirection_col line 383
  35. theorem OAI.Contingency.switchDirection_mark line 390
  36. theorem OAI.Contingency.switch_nonneg line 394
  37. def OAI.Contingency.switchTable line 412
  38. theorem OAI.Contingency.switchTable_int line 434
  39. theorem OAI.Contingency.switch_injective_with_labels line 441
  40. theorem OAI.Contingency.line_donor line 477
  41. abbrev OAI.Contingency.SmallEntryBad line 497
  42. def OAI.Contingency.rowDonor line 500
  43. theorem OAI.Contingency.rowDonor_spec line 505
  44. def OAI.Contingency.colDonor line 512
  45. theorem OAI.Contingency.colDonor_spec line 517
  46. def OAI.Contingency.smallEntryMoves line 524
  47. theorem OAI.Contingency.smallEntryMoves_injective line 536
  48. theorem OAI.Contingency.small_entry_count_floor line 572
  49. theorem OAI.Contingency.floor_donor_lower line 578
  50. theorem OAI.Contingency.small_entry_count line 587
  51. theorem OAI.Contingency.small_entry_probability line 601