OAI/Probability/SKGap/Matrix/NormalizedPrimaryRecipe.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.OrdinaryData.normalizedPrimary line 15
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.normalizedPrimary_source line 28
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.normalizedPrimary_magnetization line 34
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.normalizedPrimary_Admissible line 40
5. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.normalizedPrimary_seed line 50
6. lemma OAI.SKGapCutoff.Recipe.normalized_pair_cancel line 62
7. lemma OAI.SKGapCutoff.Recipe.scaledMean_size line 69
8. lemma OAI.SKGapCutoff.Recipe.scaledMean_difference line 76
9. lemma OAI.SKGapCutoff.Recipe.tanh_segmentRegular line 101
10. lemma OAI.SKGapCutoff.Recipe.tanh_segmentValue line 132
11. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.normalizedPrimary_coefficientClass line 139