OAI/Probability/SKGap/Localization/CoefficientRow.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.row_vectorNorm_le_opNorm line 15
2. lemma OAI.SKGapCutoff.Recipe.local_argument_row_bound line 22
3. lemma OAI.SKGapCutoff.Recipe.coefficient_row_bound line 47
4. structure OAI.SKGapCutoff.Recipe.SmallBound line 81
5. lemma OAI.SKGapCutoff.Recipe.derivativeMatrix_add line 86
6. lemma OAI.SKGapCutoff.Recipe.derivativeMatrix_sum line 90
7. lemma OAI.SKGapCutoff.Recipe.SmallBound.mono line 94
8. lemma OAI.SKGapCutoff.Recipe.SmallBound.seed line 98
9. lemma OAI.SKGapCutoff.Recipe.SmallBound.add line 104
10. lemma OAI.SKGapCutoff.Recipe.SmallBound.smul line 111
11. lemma OAI.SKGapCutoff.Recipe.SmallBound.sub line 120
12. lemma OAI.SKGapCutoff.Recipe.SmallBound.sum line 125
13. lemma OAI.SKGapCutoff.Recipe.SmallBound.coefficient line 135
14. lemma OAI.SKGapCutoff.Recipe.SmallBound.linear line 151
15. lemma OAI.SKGapCutoff.Recipe.SmallBound.primaryCorrection line 162
16. lemma OAI.SKGapCutoff.Recipe.SmallBound.auxiliaryCorrection line 170