OAI/Computability/StarHeight/TagPartitions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_nonneg line 14
2. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_mono line 17
3. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_union_le line 21
4. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.probability_iUnion_finset_le line 32
5. lemma OAI.GeneralizedStarHeight.FiniteAvoidance.exists_avoiding line 41
6. def OAI.GeneralizedStarHeight.TagPartitions.Feasible line 60
7. def OAI.GeneralizedStarHeight.TagPartitions.Satisfies line 62
8. lemma OAI.GeneralizedStarHeight.TagPartitions.feasible_partition line 65
9. def OAI.GeneralizedStarHeight.TagPartitions.repetitions line 76
10. lemma OAI.GeneralizedStarHeight.TagPartitions.repetitions_estimate line 78
11. lemma OAI.GeneralizedStarHeight.TagPartitions.repetitions_bound line 104
12. lemma OAI.GeneralizedStarHeight.TagPartitions.repetitions_pos line 115
13. lemma OAI.GeneralizedStarHeight.TagPartitions.probability_satisfies line 125
14. lemma OAI.GeneralizedStarHeight.TagPartitions.satisfies_depends line 160
15. lemma OAI.GeneralizedStarHeight.TagPartitions.probability_failure line 169
16. theorem OAI.GeneralizedStarHeight.TagPartitions.exists_partitions line 196
17. def OAI.GeneralizedStarHeight.TagPartitions.typeCount line 229
18. lemma OAI.GeneralizedStarHeight.TagPartitions.card_le_binary line 231
19. lemma OAI.GeneralizedStarHeight.TagPartitions.typeCount_bound line 241
20. lemma OAI.GeneralizedStarHeight.TagPartitions.exists_types line 257
21. lemma OAI.GeneralizedStarHeight.TagPartitions.total_count_bound line 271