OAI/Probability/SKGap/Terminal/ResidualPairMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Static.varianceEnergy_gradient_bound line 14
2. lemma OAI.SKGapCutoff.Static.weak_selftest line 24
3. lemma OAI.SKGapCutoff.Static.square_selftest line 43
4. def OAI.SKGapCutoff.Recipe.primaryPair line 59
5. lemma OAI.SKGapCutoff.Recipe.mag_vectorNorm line 62
6. lemma OAI.SKGapCutoff.Recipe.residual_vectorNorm line 71
7. lemma OAI.SKGapCutoff.Recipe.primaryPair_size line 77
8. def OAI.SKGapCutoff.Recipe.primaryPairBudget line 85
9. lemma OAI.SKGapCutoff.Recipe.primaryPairBudget_nonneg line 90
10. lemma OAI.SKGapCutoff.Recipe.primaryPair_gradient line 96
11. lemma OAI.SKGapCutoff.Recipe.primaryPair_difference_sq line 131
12. lemma OAI.SKGapCutoff.Recipe.primaryPair_scaled_difference line 138
13. theorem OAI.SKGapCutoff.Recipe.gibbs_primary_pair_moments line 148