OAI/Probability/SKGap/Matrix/StartedNodeTrace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedNodeSourceError line 18
2. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedNodeFieldError line 22
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedNodeSource_control line 28
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedNodeField_control line 56
5. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.started_derivative_error_words line 98