OAI/Probability/Localization/FirstHeavy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.FiniteEntropy.Descendant.refl line 12
2. lemma OAI.RepeatedLocalization.FiniteEntropy.Descendant.trans line 14
3. lemma OAI.RepeatedLocalization.FiniteEntropy.nested_of_point line 17
4. lemma OAI.RepeatedLocalization.FiniteEntropy.cell_eq_of_level_point line 25
5. lemma OAI.RepeatedLocalization.FiniteEntropy.Descendant.eq_of_level line 32
6. lemma OAI.RepeatedLocalization.FiniteEntropy.firstHeavy_disjoint line 36
7. lemma OAI.RepeatedLocalization.FiniteEntropy.exists_firstHeavy_ancestor line 45
8. lemma OAI.RepeatedLocalization.FiniteEntropy.measurableSet_residual line 59
9. lemma OAI.RepeatedLocalization.FiniteEntropy.measurableSet_branch line 63
10. lemma OAI.RepeatedLocalization.FiniteEntropy.branch_subset line 70
11. lemma OAI.RepeatedLocalization.FiniteEntropy.branch_disjoint line 79
12. lemma OAI.RepeatedLocalization.FiniteEntropy.attemptLetter_mem_branch line 110
13. lemma OAI.RepeatedLocalization.FiniteEntropy.attemptLetter_eq_iff line 122
14. lemma OAI.RepeatedLocalization.FiniteEntropy.heavy_disjoint_residual line 131
15. lemma OAI.RepeatedLocalization.FiniteEntropy.stopped_regular line 138