OAI/Probability/SKGap/Localization/ResidualRecipe2.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.evaluation_prefix_eq line 17
2. def OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct line 47
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_prefix line 60
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_source line 76
5. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_partial line 93
6. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_new_partial line 114
7. def OAI.SKGapCutoff.Recipe.phiCoefficient line 135
8. def OAI.SKGapCutoff.Recipe.phiDerivative line 137
9. lemma OAI.SKGapCutoff.Recipe.phiCoefficient_eq line 141
10. lemma OAI.SKGapCutoff.Recipe.base_dz line 145
11. lemma OAI.SKGapCutoff.Recipe.phiDerivative_first line 151
12. lemma OAI.SKGapCutoff.Recipe.phiDerivative_other line 157
13. def OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein line 165
14. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_source line 168
15. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_partial line 177
16. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_preserves_vanishing line 187
17. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.sum_split line 194
18. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.auxiliary_split line 199
19. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_auxiliary line 209
20. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.residual_step line 226