OAI/Probability/SKGap/Localization/SelectionDeficit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.selection_deficit_l2 line 14
2. lemma OAI.SKGapCutoff.Recipe.spin_root_direction_size line 44
3. theorem OAI.SKGapCutoff.Recipe.gibbs_residual_selection_deficit line 60
4. lemma OAI.SKGapCutoff.Recipe.uniform_cutoff_partition line 91