OAI/Probability/SKGap/Localization/SelectionPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.cutoffWeight line 15
2. def OAI.SKGapCutoff.Recipe.cutoffDeficit line 16
3. lemma OAI.SKGapCutoff.Recipe.cutoffDeficit_prod line 18
4. lemma OAI.SKGapCutoff.Recipe.cutoffDeficit_bounds line 27
5. lemma OAI.SKGapCutoff.Recipe.cutoffWeight_bounds line 33
6. lemma OAI.SKGapCutoff.Recipe.cutoffDeficit_zero_of_one line 39
7. lemma OAI.SKGapCutoff.Recipe.residualCutoff_deficit_inclusion line 43
8. lemma OAI.SKGapCutoff.Recipe.weighted_indicator_mono line 57
9. theorem OAI.SKGapCutoff.Recipe.gibbs_residual_selection_tail line 72