OAI/Probability/SKGap/Localization/StartedSmall.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.startedBudget line 14
2. lemma OAI.SKGapCutoff.Recipe.startedBudget_nonneg line 17
3. lemma OAI.SKGapCutoff.Recipe.startedBudget_ge line 23
4. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.started_evaluation_small line 34
5. def OAI.SKGapCutoff.Recipe.LocalConstants.startedNormBudget line 109
6. def OAI.SKGapCutoff.Recipe.LocalConstants.startedSourceCost line 110
7. def OAI.SKGapCutoff.Recipe.LocalConstants.startedFieldCost line 113
8. lemma OAI.SKGapCutoff.Recipe.LocalConstants.startedNormBudget_nonneg line 116
9. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.started_small line 127
10. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.started_source_control line 134
11. lemma OAI.SKGapCutoff.Recipe.LocalOrdinaryInput.started_field_control line 160