OAI/Probability/SwitchChain/CountCDF.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.CountCoupling.pairNormalizer line 10
  2. theorem OAI.Problem315.CountCoupling.pairNormalizer_pos line 13
  3. def OAI.Problem315.CountCoupling.pairProbability line 19
  4. theorem OAI.Problem315.CountCoupling.pairProbability_pos line 22
  5. theorem OAI.Problem315.CountCoupling.sum_pairProbability line 25
  6. def OAI.Problem315.CountCoupling.pairPrefix line 32
  7. theorem OAI.Problem315.CountCoupling.pairPrefix_eq_expectation line 35
  8. theorem OAI.Problem315.CountCoupling.antitone_lower_indicator line 50
  9. theorem OAI.Problem315.CountCoupling.pairPrefix_succ_le line 56
  10. theorem OAI.Problem315.CountCoupling.pairExpectation_shift_le_succ_of_antitone line 62
  11. theorem OAI.Problem315.CountCoupling.pairPrefix_le_succ_shift line 70
  12. def OAI.Problem315.CountCoupling.pairBirthMass line 78
  13. theorem OAI.Problem315.CountCoupling.pairBirthMass_nonneg line 81
  14. theorem OAI.Problem315.CountCoupling.pairBirthMass_le_probability line 85
  15. theorem OAI.Problem315.CountCoupling.pairExpectation_eq_sum_probability line 92
  16. theorem OAI.Problem315.CountCoupling.pairPrefix_zero line 101
  17. theorem OAI.Problem315.CountCoupling.pairPrefix_succ line 104
  18. theorem OAI.Problem315.CountCoupling.pairPrefix_total line 108
  19. def OAI.Problem315.CountCoupling.countObservable line 111
  20. theorem OAI.Problem315.CountCoupling.countObservable_stay_difference line 113
  21. theorem OAI.Problem315.CountCoupling.countObservable_birth_difference line 121
  22. theorem OAI.Problem315.CountCoupling.countObservable_stay_bound line 130
  23. theorem OAI.Problem315.CountCoupling.countObservable_birth_bound line 137