OAI/Probability/SKGap/Terminal/FieldGibbs.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.fieldEnergy line 15
2. def OAI.SKGapCutoff.fieldPartition line 18
3. def OAI.SKGapCutoff.fieldGibbs line 19
4. lemma OAI.SKGapCutoff.fieldPartition_pos line 22
5. lemma OAI.SKGapCutoff.fieldGibbs_pos line 24
6. lemma OAI.SKGapCutoff.sum_fieldGibbs line 26
7. lemma OAI.SKGapCutoff.fieldGibbs_zero line 30
8. lemma OAI.SKGapCutoff.fieldGibbs_edge line 33
9. lemma OAI.SKGapCutoff.fieldEnergy_flip line 41
10. lemma OAI.SKGapCutoff.fieldGibbs_detailed_balance line 48
11. lemma OAI.SKGapCutoff.Static.conditionalMean_fieldGibbs line 64
12. lemma OAI.SKGapCutoff.Static.conditionalMean_primary line 74
13. theorem OAI.SKGapCutoff.Recipe.gibbs_ordinary_residuals line 95
14. def OAI.SKGapCutoff.Recipe.vectorPair line 128
15. def OAI.SKGapCutoff.Recipe.normalizedPair line 130
16. lemma OAI.SKGapCutoff.Recipe.vectorPair_derivative line 133
17. lemma OAI.SKGapCutoff.Recipe.vectorPair_abs line 152
18. lemma OAI.SKGapCutoff.Recipe.vectorPair_cross_bound line 157
19. lemma OAI.SKGapCutoff.Recipe.vectorPair_derivative_bound line 183
20. lemma OAI.SKGapCutoff.Recipe.normalizedPair_derivative line 199
21. lemma OAI.SKGapCutoff.Recipe.normalizedPair_derivative_bound line 206