OAI/Probability/CriticalPercolation/Modular/WeightedQuery.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.SearchTree.weightedSum line 15
2. def OAI.CriticalPercolation.SearchTree.quadraticCost line 20
3. def OAI.CriticalPercolation.SearchTree.takeQuadratic line 24
4. lemma OAI.CriticalPercolation.SearchTree.quadraticCost_nonneg line 30
5. lemma OAI.CriticalPercolation.SearchTree.takeQuadratic_valid line 38
6. lemma OAI.CriticalPercolation.SearchTree.takeQuadratic_cost_le line 48
7. lemma OAI.CriticalPercolation.SearchTree.takeQuadratic_sum_eq line 62
8. lemma OAI.CriticalPercolation.SearchTree.fourthPotential_step line 80
9. lemma OAI.CriticalPercolation.SearchTree.expected_takeQuadratic_fourth_shift line 91
10. lemma OAI.CriticalPercolation.SearchTree.expected_takeQuadratic_fourth line 133