OAI/Probability/CriticalPercolation/Criticality/NormalClosureGrowth.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.SparseGrowth.eventually_exponential_dominates line 14
2. lemma OAI.CriticalPercolation.SparseGrowth.not_quadratic_exponential_lower line 27
3. def OAI.CriticalPercolation.SparseGrowth.binaryProducts line 56
4. lemma OAI.CriticalPercolation.SparseGrowth.binaryProducts_mem line 60
5. lemma OAI.CriticalPercolation.SparseGrowth.binaryProducts_card line 76
6. lemma OAI.CriticalPercolation.SparseGrowth.binaryProducts_subset_pow line 98
7. theorem OAI.CriticalPercolation.SparseGrowth.no_linear_word_strict_chain line 117
8. def OAI.CriticalPercolation.SparseGrowth.boundedConjugates line 126
9. def OAI.CriticalPercolation.SparseGrowth.conjugateStage line 129
10. lemma OAI.CriticalPercolation.SparseGrowth.mem_boundedConjugates line 132
11. lemma OAI.CriticalPercolation.SparseGrowth.boundedConjugates_mono line 136
12. lemma OAI.CriticalPercolation.SparseGrowth.conjugateStage_mono line 143
13. lemma OAI.CriticalPercolation.SparseGrowth.boundedConjugates_subset_pow line 148
14. lemma OAI.CriticalPercolation.SparseGrowth.conjugateStage_le_normalClosure line 160
15. lemma OAI.CriticalPercolation.SparseGrowth.conjugateStage_conj_generator line 167
16. lemma OAI.CriticalPercolation.SparseGrowth.conjugateStage_normal_of_stationary line 184
17. lemma OAI.CriticalPercolation.SparseGrowth.normalClosure_eq_conjugateStage_of_stationary line 205
18. theorem OAI.CriticalPercolation.SparseGrowth.exists_conjugateStage_stationary line 218
19. theorem OAI.CriticalPercolation.SparseGrowth.normalClosure_fg_of_sparse_growth line 237