OAI/Probability/SKGap/Localization/Bilinear2.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.exactG line 14
2. def OAI.SKGap.bilinearDataD line 17
3. def OAI.SKGap.bilinearDataE line 20
4. def OAI.SKGap.bilinearDataW line 22
5. def OAI.SKGap.bilinearError line 24
6. lemma OAI.SKGap.bilinearData_bound line 31
7. lemma OAI.SKGap.bilinearDataW_bound line 46
8. lemma OAI.SKGap.bilinearError_agrees line 50
9. lemma OAI.SKGap.path_all_good_exponential line 89