OAI/Probability/SKGap/Entropy/WeightedMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.cutoff_scalar_mean_bound line 14
2. lemma OAI.SKGapCutoff.Recipe.vectorNorm_le_of_unit_dot line 79
3. lemma OAI.SKGapCutoff.Recipe.gibbs_selected_direction_control line 103
4. lemma OAI.SKGapCutoff.Recipe.gibbs_selected_all_directions line 128
5. lemma OAI.SKGapCutoff.Recipe.magnetization_norm line 143
6. theorem OAI.SKGapCutoff.Recipe.gibbs_square_mean line 151