OAI/Probability/SKGap/Localization/LocalRecipeClass.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SKGapCutoff.Recipe.LocalFamilyRecipe line 19
2. lemma OAI.SKGapCutoff.Recipe.LocalFamilyRecipe.mono line 39
3. lemma OAI.SKGapCutoff.Recipe.LocalFamilyRecipe.appendStein line 45
4. lemma OAI.SKGapCutoff.Recipe.LocalFamilyRecipe.appendAuxiliary line 59
5. lemma OAI.SKGapCutoff.Recipe.LocalFamilyRecipe.appendPrimary line 68
6. lemma OAI.SKGapCutoff.Recipe.LocalFamilyRecipe.sameEnvironment line 80
7. structure OAI.SKGapCutoff.Recipe.FiniteLocalRecipeControl line 106
8. lemma OAI.SKGapCutoff.Static.LocalUniformMultiplier.congr line 131
9. lemma OAI.SKGapCutoff.Static.LocalUniformMultiplier.add line 135
10. lemma OAI.SKGapCutoff.Static.LocalUniformMultiplier.finset_sum line 151
11. lemma OAI.SKGapCutoff.Static.LocalUniformMultiplier.sum line 159