OAI/Probability/SKGap/Localization/PhiRegularity.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.affine_segment line 16
2. lemma OAI.SKGapCutoff.Recipe.affine_segmentRegular line 22
3. lemma OAI.SKGapCutoff.Recipe.phi_kernel_segmentRegular line 62
4. lemma OAI.SKGapCutoff.Recipe._root_.OAI.SKGap.Stein.RatioExpr.dBudget_nonneg line 75
5. lemma OAI.SKGapCutoff.Recipe._root_.OAI.SKGap.Stein.RatioExpr.ddBudget_nonneg line 77
6. lemma OAI.SKGapCutoff.Recipe.phi_ratio_segmentRegular line 80
7. def OAI.SKGapCutoff.Recipe.phiSelect line 91
8. lemma OAI.SKGapCutoff.Recipe.phiSelect_apply line 95
9. lemma OAI.SKGapCutoff.Recipe.phiSelect_norm line 97
10. lemma OAI.SKGapCutoff.Recipe.SegmentRegular.mono line 108
11. lemma OAI.SKGapCutoff.Recipe.fixed_root_kernel_regular line 116
12. def OAI.SKGapCutoff.Recipe.phiPairSelect line 132
13. lemma OAI.SKGapCutoff.Recipe.phiPairSelect_norm line 135
14. lemma OAI.SKGapCutoff.Recipe.two_field_kernel_regular line 142