OAI/Probability/SKGap/Localization/RecipeBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.recipeBudget line 13
2. lemma OAI.SKGapCutoff.Recipe.recipeBudget_nonneg line 16
3. def OAI.SKGapCutoff.Recipe.recipeCost line 22
4. lemma OAI.SKGapCutoff.Recipe.recipeCost_nonneg line 25
5. lemma OAI.SKGapCutoff.Recipe.recipeCost_ge line 28
6. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.evaluation_small line 39