OAI/Probability/SKGap/Localization/ConstantRecipe.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Static.UniformWeak.finset_sum line 13
2. lemma OAI.SKGapCutoff.Static.UniformSquare.finset_sum line 22
3. def OAI.SKGapCutoff.Recipe.constantRecipe line 36
4. lemma OAI.SKGapCutoff.Recipe.constantRecipe_source line 49
5. lemma OAI.SKGapCutoff.Recipe.constantRecipe_coefficients line 55
6. lemma OAI.SKGapCutoff.Recipe.constantRecipe_admissible line 63
7. lemma OAI.SKGapCutoff.Recipe.constantRecipe_family line 73
8. lemma OAI.SKGapCutoff.Recipe.primary_residual_telescope line 80
9. theorem OAI.SKGapCutoff.Recipe.gibbs_constant_residuals line 86
10. lemma OAI.SKGapCutoff.Static.UniformMultiplier.neg line 123
11. lemma OAI.SKGapCutoff.Static.UniformMultiplier.mul line 129
12. lemma OAI.SKGapCutoff.Static.UniformMultiplier.finset_prod line 136
13. def OAI.SKGapCutoff.Recipe.residualDerivativeBudget line 149
14. lemma OAI.SKGapCutoff.Recipe.residualDerivativeBudget_nonneg line 152
15. lemma OAI.SKGapCutoff.Recipe.residual_derivative_bound line 156
16. lemma OAI.SKGapCutoff.Recipe.residualCutoff_uniform line 172
17. lemma OAI.SKGapCutoff.Recipe.cutoffWeight_uniform line 195
18. lemma OAI.SKGapCutoff.Recipe.residualWeight_uniform line 201