OAI/Probability/SKGap/Localization/RecipeArgumentPullback.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.argumentSelect line 17
2. lemma OAI.SKGapCutoff.Recipe.argumentSelect_apply line 23
3. lemma OAI.SKGapCutoff.Recipe.argumentSelect_norm line 28
4. lemma OAI.SKGapCutoff.Recipe.argumentSelect_local line 38
5. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.argumentPullback line 44
6. def OAI.SKGapCutoff.Recipe.OrdinaryData.argumentPullback line 81
7. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.CoefficientClass.argumentPullback line 95
8. lemma OAI.SKGapCutoff.Recipe.argumentSelect_single_primary line 134
9. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_seedCoefficient line 152
10. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_auxCoefficient line 158
11. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_sourceOf line 163
12. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_seedPartial line 171
13. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_auxPartial line 179
14. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_partialOf line 186
15. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_fieldOf line 194
16. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.unitPullback_started_duplicate line 207