OAI/Probability/SKGap/Terminal/GibbsExpectation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.gibbsExpectation line 10
  2. def OAI.SKGapCutoff.gibbsVariance line 12
  3. def OAI.SKGapCutoff.siteVariance line 14
  4. def OAI.SKGapCutoff.dirichlet line 16
  5. def OAI.SKGapCutoff.HasGap line 18
  6. def OAI.SKGapCutoff.QuenchedGap line 21
  7. def OAI.SKGapCutoff.flip line 25
  8. lemma OAI.SKGapCutoff.flip_flip line 27
  9. lemma OAI.SKGapCutoff.spin_flip_self line 30
  10. lemma OAI.SKGapCutoff.spin_flip line 34
  11. lemma OAI.SKGapCutoff.field_flip line 40
  12. lemma OAI.SKGapCutoff.mean_flip line 45
  13. lemma OAI.SKGapCutoff.energy_flip line 49
  14. def OAI.SKGapCutoff.flipRate line 62
  15. lemma OAI.SKGapCutoff.generator_flip line 65
  16. lemma OAI.SKGapCutoff.exp_two_mul_one_sub_tanh line 77
  17. lemma OAI.SKGapCutoff.exp_neg_two_mul_one_add_tanh line 84
  18. lemma OAI.SKGapCutoff.gibbs_detailed_balance line 89
  19. def OAI.SKGapCutoff.flipEquiv line 106
  20. lemma OAI.SKGapCutoff.sum_flip line 112
  21. lemma OAI.SKGapCutoff.halfDiff_flip line 115
  22. lemma OAI.SKGapCutoff.flip_sub line 118
  23. lemma OAI.SKGapCutoff.gibbs_flip_integral line 127
  24. lemma OAI.SKGapCutoff.gibbs_generator_zero line 137
  25. lemma OAI.SKGapCutoff.gibbs_coordinate_mean line 147
  26. lemma OAI.SKGapCutoff.gibbs_edge_dirichlet line 165
  27. theorem OAI.SKGapCutoff.gibbs_dirichlet line 206