OAI/Combinatorics/BalancedRyser/Probability/CountingExposurePosterior.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.CountingExposurePosterior.expect_subtype line 14
  2. theorem OAI.Balanced.CountingExposurePosterior.expect_pi_apply line 20
  3. def OAI.Balanced.CountingExposurePosterior.exposedIndices line 36
  4. abbrev OAI.Balanced.CountingExposurePosterior.OffsetHistory line 39
  5. theorem OAI.Balanced.CountingExposurePosterior.offsetHistoryCoordinateNonempty line 43
  6. theorem OAI.Balanced.CountingExposurePosterior.expect_offset_given_history line 47
  7. abbrev OAI.Balanced.CountingExposurePosterior.Experiment line 64
  8. def OAI.Balanced.CountingExposurePosterior.countingHistory line 66
  9. def OAI.Balanced.CountingExposurePosterior.historyEquiv line 72
  10. def OAI.Balanced.CountingExposurePosterior.nextLine line 86
  11. theorem OAI.Balanced.CountingExposurePosterior.expect_history_factorization line 89
  12. theorem OAI.Balanced.CountingExposurePosterior.expect_nextLine_given_history line 111
  13. def OAI.Balanced.CountingExposurePosterior.remainingTokens line 134
  14. theorem OAI.Balanced.CountingExposurePosterior.sum_remaining_by_direction line 137
  15. theorem OAI.Balanced.CountingExposurePosterior.sum_remainingTokens line 148
  16. theorem OAI.Balanced.CountingExposurePosterior.remainingTokens_eq line 154
  17. theorem OAI.Balanced.CountingExposurePosterior.expect_remaining_by_direction line 162
  18. theorem OAI.Balanced.CountingExposurePosterior.expect_nextLine_direction_mixture line 171
  19. def OAI.Balanced.CountingExposurePosterior.usedOffsets line 182
  20. theorem OAI.Balanced.CountingExposurePosterior.nextLine_probability_eq_tokenWeight line 188
  21. theorem OAI.Balanced.CountingExposurePosterior.history_counts_le line 214
  22. theorem OAI.Balanced.CountingExposurePosterior.marked_probability_given_history_le line 227