OAI/Probability/SKGap/Localization/StartedFixed.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed line 15
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_sourceOf line 32
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_partialOf line 39
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_fieldOf line 46
5. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_started_prefix line 54
6. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_started_source line 75
7. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_seed line 83
8. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendFixed_Admissible line 88
9. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.CoefficientClass.appendFixed line 117