OAI/Probability/SKGap/Localization/UniformRecipeClass.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKGapCutoff.Recipe.FamilyRecipe line 17
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.CoefficientClass.mono line 29
3. lemma OAI.SKGapCutoff.Recipe.FamilyRecipe.mono line 41
4. lemma OAI.SKGapCutoff.Recipe.FamilyRecipe.appendStein line 46
5. lemma OAI.SKGapCutoff.Recipe.FamilyRecipe.appendAuxiliary line 55
6. lemma OAI.SKGapCutoff.Recipe.FamilyRecipe.normalizedPrimary line 61
7. lemma OAI.SKGapCutoff.Recipe.FamilyRecipe.sameEnvironment line 69
8. lemma OAI.SKGapCutoff.Static.UniformMultiplier.congr line 93
9. lemma OAI.SKGapCutoff.Static.UniformMultiplier.add line 97
10. lemma OAI.SKGapCutoff.Static.UniformMultiplier.finset_sum line 113
11. lemma OAI.SKGapCutoff.Static.UniformMultiplier.sum line 121
12. lemma OAI.SKGapCutoff.Primary.onsager_bounds line 127
13. lemma OAI.SKGapCutoff.Primary.onsager_parameter_bound line 142
14. lemma OAI.SKGapCutoff.Primary.onsager_telescope line 149