OAI/Probability/SKGap/Localization/ResidualAdmissibility.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.OrdinaryData.Admissible line 15
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.Admissible.mono line 19
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.Admissible.prefix line 24
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.Admissible.sourcePartial line 28
5. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_Admissible line 36
6. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_Admissible line 64
7. def OAI.SKGapCutoff.Recipe.OrdinaryData.appendAuxiliary line 72
8. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendAuxiliary_prefix line 79
9. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendAuxiliary_source line 88
10. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendAuxiliary_Admissible line 100
11. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.value_difference line 131
12. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.mul line 146