OAI/Probability/Contingency/DenseDyadic.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Dense Dyadic.

  1. def OAI.Contingency.Dense.BinProblem.exponent line 19
  2. theorem OAI.Contingency.Dense.BinProblem.floor_nonneg line 22
  3. theorem OAI.Contingency.Dense.BinProblem.weight_exponent line 26
  4. theorem OAI.Contingency.Dense.BinProblem.exponent_bound line 31
  5. theorem OAI.Contingency.Dense.BinProblem.neighbor_bound line 42
  6. def OAI.Contingency.Dense.BinProblem.bitKernel line 54
  7. theorem OAI.Contingency.Dense.BinProblem.bitKernel_bits line 58
  8. theorem OAI.Contingency.Dense.BinProblem.bitKernel_law line 61
  9. def OAI.Contingency.Dense.BinProblem.bitOffsets line 72
  10. theorem OAI.Contingency.Dense.BinProblem.bitOffsets_law line 75
  11. def OAI.Contingency.Dense.BinProblem.bitTrial line 78
  12. theorem OAI.Contingency.Dense.BinProblem.bitTrial_law line 84
  13. def OAI.Contingency.Dense.BinProblem.bitDraw line 106
  14. theorem OAI.Contingency.Dense.BinProblem.bitDraw_tv line 110
  15. def OAI.Contingency.Schedule.h line 130
  16. def OAI.Contingency.Schedule.T line 131
  17. def OAI.Contingency.Schedule.Jo line 132
  18. def OAI.Contingency.Schedule.Q line 133
  19. def OAI.Contingency.Schedule.qs line 134
  20. def OAI.Contingency.Schedule.rmax line 135
  21. def OAI.Contingency.Schedule.H line 136
  22. def OAI.Contingency.Schedule.JD line 137
  23. def OAI.Contingency.Schedule.R1 line 138
  24. def OAI.Contingency.Schedule.RD line 139
  25. def OAI.Contingency.Schedule.RT line 140
  26. def OAI.Contingency.Schedule.R line 141
  27. theorem OAI.Contingency.Schedule.clog_self_bound line 143
  28. theorem OAI.Contingency.Schedule.qs_bound line 146
  29. theorem OAI.Contingency.Schedule.bounds line 154
  30. theorem OAI.Contingency.Dense.BinProblem.bitTrial_bits line 245
  31. theorem OAI.Contingency.Dense.BinProblem.bitOffsets_bound line 252
  32. theorem OAI.Contingency.Dense.BinProblem.bitTrial_bound line 266
  33. theorem OAI.Contingency.Dense.BinProblem.bitDraw_bound line 272
  34. def OAI.Contingency.Dense.BinProblem.reservedDraw line 281
  35. theorem OAI.Contingency.Dense.BinProblem.reservedDraw_bits line 285
  36. theorem OAI.Contingency.Dense.BinProblem.reservedDraw_tv line 288
  37. lemma OAI.Contingency.Dense.floor_width_bounds line 309
  38. abbrev OAI.Contingency.Dense.sortedR line 330
  39. abbrev OAI.Contingency.Dense.sortedP line 331
  40. def OAI.Contingency.Dense.literalWidth line 333
  41. theorem OAI.Contingency.Dense.padding_scale line 338
  42. abbrev OAI.Contingency.Dense.literalProblem line 342
  43. theorem OAI.Contingency.Dense.literalWidth_bound line 373
  44. def OAI.Contingency.Dense.literalDraw line 378
  45. theorem OAI.Contingency.Dense.literalDraw_bits line 384
  46. theorem OAI.Contingency.Dense.literalDraw_tv line 389
  47. def OAI.Contingency.PaddedGraph.IsLarge line 419
  48. def OAI.Contingency.PaddedGraph.IsSmall line 422
  49. instance OAI.Contingency.PaddedGraph.(instance at line 425) line 425
  50. instance OAI.Contingency.PaddedGraph.(instance at line 427) line 427
  51. structure OAI.Contingency.PaddedGraph.State line 432
  52. def OAI.Contingency.PaddedGraph.rowSum line 437
  53. def OAI.Contingency.PaddedGraph.colSum line 438
  54. def OAI.Contingency.PaddedGraph.Feasible line 440
  55. def OAI.Contingency.PaddedGraph.Transversal line 446
  56. def OAI.Contingency.PaddedGraph.unit line 448
  57. def OAI.Contingency.PaddedGraph.DefectAt line 450
  58. def OAI.Contingency.PaddedGraph.receiver line 455
  59. def OAI.Contingency.PaddedGraph.repair line 458
  60. theorem OAI.Contingency.PaddedGraph.repair_transversal line 463
  61. theorem OAI.Contingency.PaddedGraph.rowSum_unit line 466
  62. theorem OAI.Contingency.PaddedGraph.colSum_unit line 475
  63. theorem OAI.Contingency.PaddedGraph.rowSum_sub_add line 484
  64. theorem OAI.Contingency.PaddedGraph.colSum_sub_add line 488
  65. theorem OAI.Contingency.PaddedGraph.donor_positive line 492
  66. theorem OAI.Contingency.PaddedGraph.repair_nonneg line 501
  67. theorem OAI.Contingency.PaddedGraph.repair_support line 513
  68. theorem OAI.Contingency.PaddedGraph.repair_rowSum line 529
  69. theorem OAI.Contingency.PaddedGraph.repair_q_identity line 547
  70. theorem OAI.Contingency.PaddedGraph.repair_colSum line 557
  71. theorem OAI.Contingency.PaddedGraph.coordinate_le_rowSum line 574
  72. theorem OAI.Contingency.PaddedGraph.coordinate_le_colSum line 578
  73. theorem OAI.Contingency.PaddedGraph.repair_feasible line 584
  74. theorem OAI.Contingency.PaddedGraph.repair_injective line 629
  75. def OAI.Contingency.PaddedGraph.Before line 644
  76. theorem OAI.Contingency.PaddedGraph.before_ne line 646
  77. theorem OAI.Contingency.PaddedGraph.before_trans line 653
  78. theorem OAI.Contingency.PaddedGraph.receiver_order line 660
  79. theorem OAI.Contingency.PaddedGraph.repair_prefix line 666
  80. theorem OAI.Contingency.PaddedGraph.repair_special line 681