OAI/Combinatorics/TreeEdit/FiniteProbability.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TreeEdit.FiniteProbability.mean line 9
  2. lemma OAI.TreeEdit.FiniteProbability.mean_nonneg line 12
  3. lemma OAI.TreeEdit.FiniteProbability.mean_le line 15
  4. lemma OAI.TreeEdit.FiniteProbability.mean_const line 18
  5. lemma OAI.TreeEdit.FiniteProbability.mean_add line 22
  6. lemma OAI.TreeEdit.FiniteProbability.mean_mul_const line 25
  7. lemma OAI.TreeEdit.FiniteProbability.mean_sum line 28
  8. lemma OAI.TreeEdit.FiniteProbability.mean_prod line 33
  9. def OAI.TreeEdit.FiniteProbability.probability line 41
  10. lemma OAI.TreeEdit.FiniteProbability.probability_nonneg line 44
  11. lemma OAI.TreeEdit.FiniteProbability.probability_le_one line 48
  12. lemma OAI.TreeEdit.FiniteProbability.probability_not line 53
  13. lemma OAI.TreeEdit.FiniteProbability.probability_mono line 66
  14. lemma OAI.TreeEdit.FiniteProbability.probability_union_bound line 73
  15. lemma OAI.TreeEdit.FiniteProbability.probability_exists line 88
  16. lemma OAI.TreeEdit.FiniteProbability.mean_equiv line 94
  17. lemma OAI.TreeEdit.FiniteProbability.mean_pair line 100
  18. lemma OAI.TreeEdit.FiniteProbability.probability_eq line 110
  19. lemma OAI.TreeEdit.FiniteProbability.probability_eq_of_uniform line 114
  20. lemma OAI.TreeEdit.FiniteProbability.perm_eval_probability line 130
  21. lemma OAI.TreeEdit.FiniteProbability.permutation_avoidance line 143
  22. lemma OAI.TreeEdit.FiniteProbability.markov line 152
  23. lemma OAI.TreeEdit.FiniteProbability.independent_lower_tail line 163
  24. lemma OAI.TreeEdit.FiniteProbability.mean_fiberwise line 204
  25. lemma OAI.TreeEdit.FiniteProbability.probability_comp_uniform line 213
  26. lemma OAI.TreeEdit.FiniteProbability.probability_subsingleton line 220
  27. lemma OAI.TreeEdit.FiniteProbability.hom_uniform line 229
  28. lemma OAI.TreeEdit.FiniteProbability.probability_pair line 245
  29. lemma OAI.TreeEdit.FiniteProbability.independent_lower_tail_subset line 248
  30. lemma OAI.TreeEdit.FiniteProbability.pair_success_lower line 294
  31. lemma OAI.TreeEdit.FiniteProbability.pair_failure_bound line 305