OAI/Probability/SKGap/Localization/RecipeIncrement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.finite_sum_fourth line 15
2. lemma OAI.SKGapCutoff.Recipe.primaryIncrement_fourth line 26
3. lemma OAI.SKGapCutoff.Recipe.primaryIncrement_row line 48
4. lemma OAI.SKGapCutoff.Recipe.primaryIncrement_diagonal line 62
5. lemma OAI.SKGapCutoff.Recipe.parameterIncrement_bound line 76
6. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.partial_difference line 101
7. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.partial_row line 119
8. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.coefficient_bound line 133
9. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.partial_bound_coefficient line 144