OAI/Probability/Contingency/GreedyTable.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Greedy Table.

  1. def OAI.Contingency.marginPrefix line 15
  2. theorem OAI.Contingency.marginPrefix_zero line 18
  3. theorem OAI.Contingency.marginPrefix_total line 21
  4. theorem OAI.Contingency.marginPrefix_mono line 24
  5. theorem OAI.Contingency.marginPrefix_succ line 34
  6. def OAI.Contingency.intervalOverlap line 50
  7. theorem OAI.Contingency.intervalOverlap_symm line 52
  8. theorem OAI.Contingency.intervalOverlap_increment line 56
  9. theorem OAI.Contingency.prefix_increments_sum line 61
  10. def OAI.Contingency.greedyEntries line 72
  11. theorem OAI.Contingency.greedyEntries_row line 76
  12. theorem OAI.Contingency.greedyEntries_col line 96
  13. def OAI.Contingency.greedyTable line 104
  14. def OAI.Contingency.PaddedGraph.greedyCompletion line 121
  15. def OAI.Contingency.PaddedGraph.positiveLargeEquiv line 133
  16. def OAI.Contingency.PaddedGraph.canonicalDraw line 149
  17. theorem OAI.Contingency.PaddedGraph.canonicalDraw_bits line 165
  18. theorem OAI.Contingency.PaddedGraph.canonicalDraw_tv line 173
  19. theorem OAI.Contingency.Law.point_tv line 202
  20. theorem OAI.Contingency.Law.correction_domination line 217
  21. def OAI.Contingency.correctionCount line 236
  22. theorem OAI.Contingency.correction_integer_domination line 239
  23. theorem OAI.Contingency.correction_counts line 265
  24. def OAI.Contingency.correctionLaw line 279
  25. theorem OAI.Contingency.corrected_exact line 291
  26. def OAI.Contingency.IntegerDraw.total line 318
  27. def OAI.Contingency.IntegerDraw.scan line 324
  28. def OAI.Contingency.IntegerDraw.weight line 328
  29. theorem OAI.Contingency.IntegerDraw.scan_none_iff line 331
  30. theorem OAI.Contingency.IntegerDraw.scan_some_lt line 340
  31. theorem OAI.Contingency.IntegerDraw.scan_count line 347
  32. theorem OAI.Contingency.IntegerDraw.scan_count_padded line 367
  33. def OAI.Contingency.IntegerDraw.trial line 379
  34. theorem OAI.Contingency.IntegerDraw.trial_count line 382
  35. def OAI.Contingency.IntegerDraw.visits line 390
  36. theorem OAI.Contingency.IntegerDraw.visits_le line 394
  37. theorem OAI.Contingency.IntegerDraw.subtraction_bound line 404
  38. def OAI.Contingency.IntegerDraw.entries line 419
  39. theorem OAI.Contingency.IntegerDraw.total_eq_sum line 422
  40. theorem OAI.Contingency.IntegerDraw.entries_total line 428
  41. theorem OAI.Contingency.IntegerDraw.entries_weight line 432
  42. theorem OAI.Contingency.IntegerDraw.word_bound line 435
  43. def OAI.Contingency.IntegerDraw.bits line 446
  44. def OAI.Contingency.IntegerDraw.drawTrial line 447
  45. theorem OAI.Contingency.IntegerDraw.drawTrial_some line 449
  46. theorem OAI.Contingency.IntegerDraw.drawTrial_none line 454
  47. def OAI.Contingency.IntegerDraw.failure line 461
  48. theorem OAI.Contingency.IntegerDraw.failure_bounds line 463
  49. def OAI.Contingency.IntegerDraw.stoppingMass line 479
  50. theorem OAI.Contingency.IntegerDraw.rejection_tail line 481
  51. theorem OAI.Contingency.IntegerDraw.rejection_summable line 485
  52. theorem OAI.Contingency.IntegerDraw.expected_words line 490
  53. theorem OAI.Contingency.IntegerDraw.rejection_exact line 496
  54. theorem OAI.Contingency.table_entry_le_total line 523
  55. theorem OAI.Contingency.table_card_cap line 528
  56. theorem OAI.Contingency.table_card_dyadic line 541
  57. def OAI.Contingency.Parameters.D line 551
  58. theorem OAI.Contingency.Parameters.rare_exponent line 553
  59. theorem OAI.Contingency.Parameters.rare_weight line 563
  60. theorem OAI.Contingency.Parameters.table_card_D line 569
  61. theorem OAI.Contingency.correction_accuracy_positive line 597
  62. def OAI.Contingency.canonicalResidual line 606
  63. theorem OAI.Contingency.canonicalResidual_sum line 608
  64. theorem OAI.Contingency.canonicalResidual_formula line 614
  65. theorem OAI.Contingency.canonicalResidual_pos_total line 622
  66. theorem OAI.Contingency.canonical_corrected_exact line 629
  67. theorem OAI.Contingency.canonical_rejection_termination line 645