OAI/Probability/Contingency/DirectCases.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Direct Cases.

  1. def OAI.Contingency.DirectCase line 16
  2. theorem OAI.Contingency.table_subsingleton_of_direct line 18
  3. theorem OAI.Contingency.Law.uniform_subsingleton line 50
  4. def OAI.Contingency.arbitraryDraw line 63
  5. theorem OAI.Contingency.arbitraryDraw_bits line 71
  6. theorem OAI.Contingency.arbitraryDraw_tv line 81
  7. def OAI.Contingency.IntegerTabulation.step line 107
  8. def OAI.Contingency.IntegerTabulation.propagate line 110
  9. def OAI.Contingency.IntegerTabulation.propagationOps line 116
  10. theorem OAI.Contingency.IntegerTabulation.propagationOps_eq line 120
  11. theorem OAI.Contingency.IntegerTabulation.step_total line 125
  12. theorem OAI.Contingency.IntegerTabulation.propagate_total line 132
  13. theorem OAI.Contingency.IntegerTabulation.propagate_entry_bound line 139
  14. theorem OAI.Contingency.IntegerTabulation.partial_step_bound line 147
  15. theorem OAI.Contingency.IntegerTabulation.propagate_walk line 155
  16. def OAI.Contingency.IntegerTabulation.stoppedVector line 167
  17. theorem OAI.Contingency.IntegerTabulation.stoppedVector_eq line 171
  18. theorem OAI.Contingency.IntegerTabulation.stoppedVector_total line 177
  19. theorem OAI.Contingency.IntegerTabulation.stoppedVector_bound line 184
  20. def OAI.Contingency.PaddedGraph.graphArray line 202
  21. theorem OAI.Contingency.PaddedGraph.graphArray_injective line 207
  22. theorem OAI.Contingency.PaddedGraph.graph_card_array line 226
  23. theorem OAI.Contingency.PaddedGraph.graph_card_dyadic line 230
  24. def OAI.Contingency.PaddedGraph.completionArray line 241
  25. theorem OAI.Contingency.PaddedGraph.completion_card_cap line 248
  26. theorem OAI.Contingency.PaddedGraph.completion_card_dyadic line 263
  27. def OAI.Contingency.BinaryArithmetic.succCost line 286
  28. theorem OAI.Contingency.BinaryArithmetic.succCost_le line 291
  29. theorem OAI.Contingency.BinaryArithmetic.succ_size_le line 294
  30. theorem OAI.Contingency.BinaryArithmetic.add_size_le line 298
  31. def OAI.Contingency.BinaryArithmetic.addCost line 320
  32. theorem OAI.Contingency.BinaryArithmetic.addCost_le line 328
  33. def OAI.Contingency.BinaryArithmetic.mulCost line 350
  34. theorem OAI.Contingency.BinaryArithmetic.mul_size_le line 355
  35. theorem OAI.Contingency.BinaryArithmetic.mulCost_le line 361
  36. theorem OAI.Contingency.BinaryArithmetic.add_certificate line 379
  37. theorem OAI.Contingency.BinaryArithmetic.mul_certificate line 383
  38. def OAI.Contingency.BinaryArithmetic.numAddCost line 398
  39. def OAI.Contingency.BinaryArithmetic.numMulCost line 403
  40. theorem OAI.Contingency.BinaryArithmetic.numAddCost_le line 408
  41. theorem OAI.Contingency.BinaryArithmetic.numMulCost_le line 419
  42. theorem OAI.Contingency.BinaryArithmetic.numSize_le_of_lt line 436
  43. def OAI.Contingency.BinaryArithmetic.binaryDot line 446
  44. def OAI.Contingency.BinaryArithmetic.dotValue line 453
  45. theorem OAI.Contingency.BinaryArithmetic.binaryDot_value line 455
  46. theorem OAI.Contingency.BinaryArithmetic.binaryDot_cost line 465
  47. def OAI.Contingency.BinaryArithmetic.binaryColumn line 490
  48. theorem OAI.Contingency.BinaryArithmetic.binaryColumn_value line 493
  49. def OAI.Contingency.BinaryArithmetic.binaryPropagate line 499
  50. theorem OAI.Contingency.BinaryArithmetic.binaryPropagate_value line 505
  51. theorem OAI.Contingency.BinaryArithmetic.denominator_size line 527
  52. theorem OAI.Contingency.BinaryArithmetic.binaryColumn_cost line 531
  53. def OAI.Contingency.BinaryArithmetic.binaryPropagationCost line 567
  54. theorem OAI.Contingency.BinaryArithmetic.binaryPropagationCost_le_aux line 572
  55. theorem OAI.Contingency.BinaryArithmetic.binaryPropagationCost_le line 592