OAI/Probability/SKGap/Localization/RecipeError.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SKGapCutoff.Recipe.sourceError_rearrangeline 19 - def
OAI.SKGapCutoff.Recipe.OrdinaryData.sourceAtomsline 31 - lemma
OAI.SKGapCutoff.Recipe.OrdinaryData.sourceOf_derivativeline 35 - def
OAI.SKGapCutoff.Recipe.OrdinaryData.sourceDerivativeErrorline 70 - def
OAI.SKGapCutoff.Recipe.OrdinaryData.fieldDerivativeErrorline 73 - lemma
OAI.SKGapCutoff.Recipe.OrdinaryData.source_error_recursionline 76 - lemma
OAI.SKGapCutoff.Recipe.OrdinaryData.fieldOf_derivativeline 86 - lemma
OAI.SKGapCutoff.Recipe.OrdinaryData.field_error_recursionline 110