OAI/Probability/SKGap/Localization/ResidualSelection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Recipe.residualEnergy line 14
2. lemma OAI.SKGapCutoff.Recipe.residualEnergy_nonneg line 17
3. lemma OAI.SKGapCutoff.Recipe.residualEnergy_eq line 20
4. lemma OAI.SKGapCutoff.Recipe.residualEnergy_sum line 32
5. lemma OAI.SKGapCutoff.Recipe.residualEnergy_sum_le line 41
6. lemma OAI.SKGapCutoff.Recipe.sum_range_pairs line 57
7. lemma OAI.SKGapCutoff.Recipe.disjoint_small_pair line 66
8. lemma OAI.SKGapCutoff.Recipe.small_residual_pair line 85