OAI/Combinatorics/ThinTrees/ExtractionBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StrongThinTree.extractQ line 11
2. def OAI.StrongThinTree.errorU line 12
3. def OAI.StrongThinTree.resistanceT line 13
4. lemma OAI.StrongThinTree.extractQ_bounds line 15
5. lemma OAI.StrongThinTree.negative_power_q_bound line 31
6. lemma OAI.StrongThinTree.extract_response_ratio line 41
7. lemma OAI.StrongThinTree.eventual_extraction_numeric line 72