OAI/Combinatorics/IndependentSets/Expansion/PoweringReturn.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.portConsEquiv line 14
2. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_word_cons_head line 27
3. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_word_cons_tail line 35
4. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.iterateOperator_succ_right line 43
5. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_wordEnd line 50
6. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_pivot_endpoints line 71
7. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_edge_endpoints line 113
8. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.bit_bool line 137
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_edge_bit line 140
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.mean_marked_bit line 144
11. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.edgeAt_zero line 154
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.word_first_hit_mean line 158
13. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.word_hit_mean line 169
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.word_pair_hit_mean line 196
15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.hit_mean line 254
16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.pair_hit_mean line 270
17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringReturn.pair_event_mean line 291