OAI/Combinatorics/CliqueFree/Lottery.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CliqueFreeIndependence.Lottery.Law line 18

   Source documentation

   A finite real lottery; list entries need not have distinct outcomes.

   abbrev Law (α : Type u) := List (ℝ × α)

2. def OAI.CliqueFreeIndependence.Lottery.expect line 20
3. def OAI.CliqueFreeIndependence.Lottery.Positive line 22
4. def OAI.CliqueFreeIndependence.Lottery.total line 24
5. def OAI.CliqueFreeIndependence.Lottery.IsProb line 26
6. lemma OAI.CliqueFreeIndependence.Lottery.expect_nil line 28
7. lemma OAI.CliqueFreeIndependence.Lottery.expect_cons line 29
8. lemma OAI.CliqueFreeIndependence.Lottery.expect_singleton line 31
9. lemma OAI.CliqueFreeIndependence.Lottery.expect_append line 34
10. lemma OAI.CliqueFreeIndependence.Lottery.expect_add line 37
11. lemma OAI.CliqueFreeIndependence.Lottery.expect_mul line 46
12. lemma OAI.CliqueFreeIndependence.Lottery.expect_const line 55
13. lemma OAI.CliqueFreeIndependence.Lottery.expect_mono line 58
14. lemma OAI.CliqueFreeIndependence.Lottery.expect_sum line 66
15. def OAI.CliqueFreeIndependence.Lottery.transform line 73
16. lemma OAI.CliqueFreeIndependence.Lottery.expect_transform line 75
17. lemma OAI.CliqueFreeIndependence.Lottery.total_transform line 85
18. lemma OAI.CliqueFreeIndependence.Lottery.positive_transform line 88
19. lemma OAI.CliqueFreeIndependence.Lottery.positive_append line 94