OAI/Probability/CriticalPercolation/ProductMeasure/QueryMartingale.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.SearchTree.queryCount line 15
2. def OAI.CriticalPercolation.SearchTree.centeredSum line 19
3. def OAI.CriticalPercolation.SearchTree.truncate line 23
4. lemma OAI.CriticalPercolation.SearchTree.truncate_valid line 28
5. lemma OAI.CriticalPercolation.SearchTree.queryCount_truncate_le line 37
6. lemma OAI.CriticalPercolation.SearchTree.centeredSum_truncate_eq line 48
7. lemma OAI.CriticalPercolation.SearchTree.centeredSum_moments line 70
8. lemma OAI.CriticalPercolation.SearchTree.truncated_second_le line 104