OAI/Probability/CriticalPercolation/Exploration/QueryBand.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CriticalPercolation.FiniteProduct.expect_abs_sq_leline 15 - lemma
OAI.CriticalPercolation.FiniteProduct.expect_abs_le_of_second_leline 25 - lemma
OAI.CriticalPercolation.SearchTree.queryCount_eq_reads_lengthline 37 - lemma
OAI.CriticalPercolation.SearchTree.centeredSum_eq_zero_of_countline 44 - lemma
OAI.CriticalPercolation.SearchTree.queryCount_le_cardline 52 - lemma
OAI.CriticalPercolation.SearchTree.band_centered_boundline 57