OAI/Probability/Contingency/LawComposition.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

Law Composition.

  1. theorem OAI.Contingency.Law.pure_bind line 16
  2. theorem OAI.Contingency.Law.bind_assoc line 21
  3. theorem OAI.Contingency.Law.map_bind line 27
  4. theorem OAI.Contingency.Law.map_map line 31
  5. def OAI.Contingency.Tables line 50
  6. instance OAI.Contingency.tablesFinite line 54
  7. def OAI.Contingency.encodeNat line 70
  8. def OAI.Contingency.encodeList line 73
  9. def OAI.Contingency.inputBits line 75
  10. def OAI.Contingency.outputBits line 78
  11. inductive OAI.Contingency.BitModel.Move line 84
  12. structure OAI.Contingency.BitModel.Tape line 89
  13. def OAI.Contingency.BitModel.Tape.blank line 95
  14. def OAI.Contingency.BitModel.Tape.ofInput line 97
  15. def OAI.Contingency.BitModel.Tape.move line 102
  16. structure OAI.Contingency.BitModel.Instruction line 114
  17. structure OAI.Contingency.BitModel.Machine line 122
  18. structure OAI.Contingency.BitModel.Config line 129
  19. def OAI.Contingency.BitModel.Machine.initial line 134
  20. def OAI.Contingency.BitModel.Machine.step line 137
  21. def OAI.Contingency.BitModel.Machine.run line 145
  22. def OAI.Contingency.BitModel.Machine.mass line 150
  23. def OAI.Contingency.BitModel.Machine.tail line 156
  24. def OAI.Contingency.inputSize line 164
  25. def OAI.Contingency.variationBy line 166
  26. def OAI.Contingency.BoundedMain line 174
  27. def OAI.Contingency.ExactMain line 187
  28. def OAI.Contingency.MainTheorem line 203
  29. theorem OAI.Contingency.tables_nonempty line 217
  30. lemma OAI.Contingency.sum_dite_subtype line 262
  31. theorem OAI.Contingency.table_cell_le_row line 275
  32. theorem OAI.Contingency.table_cell_le_col line 279
  33. def OAI.Contingency.restrictTable line 287
  34. def OAI.Contingency.expandTable line 315
  35. def OAI.Contingency.restrictTableEquiv line 336
  36. def OAI.Contingency.maximizers line 363
  37. theorem OAI.Contingency.maximizers_nonempty line 366
  38. def OAI.Contingency.maximumIndex line 371
  39. theorem OAI.Contingency.maximumIndex_max line 373
  40. theorem OAI.Contingency.maximumIndex_first line 377
  41. def OAI.Contingency.marginOrder line 380
  42. theorem OAI.Contingency.marginOrder_max line 383
  43. def OAI.Contingency.permuteTable line 390
  44. def OAI.Contingency.permuteTableEquiv line 394
  45. theorem OAI.Contingency.Law.uniform_map_equiv line 410
  46. def OAI.Contingency.Dense.complete line 432
  47. theorem OAI.Contingency.Dense.complete_free line 439
  48. theorem OAI.Contingency.Dense.complete_right line 443
  49. theorem OAI.Contingency.Dense.complete_bottom line 447
  50. theorem OAI.Contingency.Dense.complete_corner line 451
  51. theorem OAI.Contingency.Dense.complete_row line 456
  52. theorem OAI.Contingency.Dense.complete_col line 467
  53. theorem OAI.Contingency.Dense.complete_represents line 480
  54. def OAI.Contingency.Dense.scale line 509
  55. def OAI.Contingency.Dense.scaled line 512
  56. def OAI.Contingency.Dense.normalized line 516
  57. def OAI.Contingency.Dense.polytope line 520
  58. theorem OAI.Contingency.Dense.width_bounds line 525
  59. theorem OAI.Contingency.Dense.entry_le_scale line 539
  60. theorem OAI.Contingency.Dense.polytope_bounded line 547
  61. theorem OAI.Contingency.Dense.real_completion line 586
  62. theorem OAI.Contingency.Dense.interior_table line 613
  63. theorem OAI.Contingency.Dense.interior_point line 652