OAI/Probability/Contingency/SafeBins.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

Safe Bins.

  1. def OAI.Contingency.Grid.closedBin line 19
  2. def OAI.Contingency.Grid.safeBins line 22
  3. theorem OAI.Contingency.Grid.mem_safeBins line 26
  4. theorem OAI.Contingency.Grid.closedBin_distance line 29
  5. theorem OAI.Contingency.Grid.inner_bin_safe line 40
  6. theorem OAI.Contingency.Grid.boxes_volume_le_card line 51
  7. theorem OAI.Contingency.Grid.safe_bin_count line 60
  8. theorem OAI.Contingency.Grid.corner_mem_closedBin line 77
  9. theorem OAI.Contingency.Grid.safe_bin_weight_one line 81
  10. theorem OAI.Contingency.Dense.dense_safe_bin_bound line 112
  11. def OAI.Contingency.Dense.integerComplete line 169
  12. theorem OAI.Contingency.Dense.integerComplete_cast line 176
  13. theorem OAI.Contingency.Dense.integerComplete_nonneg line 183
  14. def OAI.Contingency.Dense.tableOfFree line 189
  15. theorem OAI.Contingency.Dense.tableOfFree_free line 207
  16. theorem OAI.Contingency.Dense.tables_free_injective line 213
  17. abbrev OAI.Contingency.Dense.Offsets line 228
  18. abbrev OAI.Contingency.Dense.Sample line 229
  19. def OAI.Contingency.Dense.freeSample line 231
  20. def OAI.Contingency.Dense.samplePoint line 234
  21. theorem OAI.Contingency.Dense.samplePoint_mem line 237
  22. theorem OAI.Contingency.Dense.samplePoint_complete line 247
  23. theorem OAI.Contingency.Dense.freeSample_injective line 258
  24. theorem OAI.Contingency.Dense.closedBin_corner_distance line 287
  25. theorem OAI.Contingency.Dense.feasible_bin_weight_one line 297
  26. def OAI.Contingency.Dense.Accepted line 319
  27. theorem OAI.Contingency.Dense.accepted_iff_point line 323
  28. theorem OAI.Contingency.Dense.safe_bin_accepted line 343
  29. theorem OAI.Contingency.Dense.table_bin_bound line 352
  30. def OAI.Contingency.Dense.encodeSample line 365
  31. theorem OAI.Contingency.Dense.encodeSample_free line 372
  32. theorem OAI.Contingency.Dense.encodeSample_accepted line 381
  33. def OAI.Contingency.Dense.acceptedEquiv line 392
  34. structure OAI.Contingency.Dense.BinProblem line 426
  35. def OAI.Contingency.Dense.BinProblem.widths line 449
  36. def OAI.Contingency.Dense.BinProblem.weight line 450
  37. def OAI.Contingency.Dense.BinProblem.Z line 451
  38. def OAI.Contingency.Dense.BinProblem.offsetCount line 452
  39. def OAI.Contingency.Dense.BinProblem.sampleMass line 453
  40. def OAI.Contingency.Dense.BinProblem.good line 454
  41. def OAI.Contingency.Dense.BinProblem.success line 456
  42. theorem OAI.Contingency.Dense.BinProblem.offsetCount_pos line 460
  43. theorem OAI.Contingency.Dense.BinProblem.Kpos line 465
  44. theorem OAI.Contingency.Dense.BinProblem.weight_pos line 470
  45. theorem OAI.Contingency.Dense.BinProblem.Zpos line 472
  46. theorem OAI.Contingency.Dense.BinProblem.sampleMass_nonneg line 476
  47. theorem OAI.Contingency.Dense.BinProblem.sampleMass_total line 480
  48. theorem OAI.Contingency.Dense.BinProblem.widthlo line 486
  49. theorem OAI.Contingency.Dense.BinProblem.widthhi line 490
  50. theorem OAI.Contingency.Dense.BinProblem.dim line 494
  51. theorem OAI.Contingency.Dense.BinProblem.accepted_weight line 498
  52. def OAI.Contingency.Dense.BinProblem.safe line 506
  53. theorem OAI.Contingency.Dense.BinProblem.safe_count line 508
  54. theorem OAI.Contingency.Dense.BinProblem.safe_success line 515
  55. theorem OAI.Contingency.Dense.BinProblem.success_lower line 519
  56. theorem OAI.Contingency.Dense.BinProblem.success_upper line 544
  57. theorem OAI.Contingency.Dense.BinProblem.bound line 552
  58. def OAI.Contingency.Dense.BinProblem.tableSample line 555
  59. theorem OAI.Contingency.Dense.BinProblem.table_mass line 558
  60. theorem OAI.Contingency.Dense.BinProblem.success_eq_card line 563
  61. theorem OAI.Contingency.Dense.BinProblem.conditional_uniform line 578