OAI/Probability/SKGap/Localization/StartedGraph.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedTree line 17
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedTree_pos line 27
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedTree_leafMass line 35
4. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedRetainedSource line 44
5. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedRetainedField line 45
6. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedRetainedSource_eq line 47
7. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedRetainedField_eq line 55
8. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.started_prediction_zero line 67
9. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedSourceError line 88
10. def OAI.SKGapCutoff.Recipe.OrdinaryData.startedFieldError line 90
11. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.started_source_error_recursion line 93
12. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.started_field_error_recursion line 103
13. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedSourceError_zero line 114
14. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.startedFieldError_zero line 117