OAI/Probability/SKGap/Entropy/NormalizedWeightedMean.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.squareMass line 14
2. def OAI.SKGapCutoff.Recipe.squareMean line 17
3. lemma OAI.SKGapCutoff.Recipe.squareMass_probability line 20
4. lemma OAI.SKGapCutoff.Recipe.squareMean_centered line 26
5. lemma OAI.SKGapCutoff.Recipe.normalized_square_bound line 34
6. theorem OAI.SKGapCutoff.Recipe.gibbs_normalized_square_mean line 58
7. structure OAI.SKGapCutoff.Recipe.StableRecipeInstance line 89
8. theorem OAI.SKGapCutoff.Recipe.uniform_stable_square_mean line 100
9. lemma OAI.SKGapCutoff.Recipe.choose_selection_depth line 123