OAI/Probability/SKGap/Localization/GeneralTemplateRegularity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.generalTemplateMatrix line 13
2. def OAI.SKGap.generalTemplateHolder line 17
3. lemma OAI.SKGap.generalTemplateHolder_nonneg line 20
4. theorem OAI.SKGap.generalTemplateMatrix_increments line 25
5. lemma OAI.SKGap.wordParameter_dist_le_one line 55
6. def OAI.SKGap.templateMatrix line 61
7. def OAI.SKGap.templateHolder line 65
8. lemma OAI.SKGap.templateHolder_nonneg line 67
9. lemma OAI.SKGap.templateFactor_pair line 73
10. theorem OAI.SKGap.templateMatrix_increments line 127