OAI/Probability/SKBarriers/SpinGlass/Basic.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.MainStatement line 13
  2. def OAI.SK.overlap line 17
  3. def OAI.SK.flip line 20
  4. theorem OAI.SK.spin_not line 22
  5. theorem OAI.SK.spin_sq line 25
  6. theorem OAI.SK.flip_flip line 28
  7. theorem OAI.SK.hamiltonian_flip line 32
  8. theorem OAI.SK.gibbs_flip line 36
  9. theorem OAI.SK.partition_pos line 40
  10. theorem OAI.SK.gibbs_pos line 44
  11. theorem OAI.SK.gibbs_sum line 48
  12. theorem OAI.SK.overlap_flip_right line 53
  13. theorem OAI.SK.overlap_comm line 57
  14. instance OAI.SK.disorderLaw_probability line 60
  15. theorem OAI.SK.disorder_coordinate_law line 64
  16. theorem OAI.SK.disorder_coordinate_gaussian line 68
  17. theorem OAI.SK.disorder_independent line 72
  18. theorem OAI.SK.disorder_gaussian line 76
  19. theorem OAI.SK.hamiltonian_gaussian line 79
  20. theorem OAI.SK.hamiltonian_integrable line 99
  21. theorem OAI.SK.disorder_mean_zero line 103
  22. theorem OAI.SK.hamiltonian_mean_zero line 108
  23. theorem OAI.SK.disorder_covariance line 116
  24. theorem OAI.SK.hamiltonian_covariance_edges line 129
  25. theorem OAI.SK.sum_edges line 158
  26. theorem OAI.SK.sum_sq_eq_edges line 166
  27. theorem OAI.SK.overlap_self line 200
  28. theorem OAI.SK.hamiltonian_covariance line 205
  29. theorem OAI.SK.disorder_linear_gaussian line 230
  30. theorem OAI.SK.hamiltonian_add_gaussian line 237
  31. theorem OAI.SK.hamiltonian_variance line 250
  32. theorem OAI.SK.gaussian_exp_integral line 256
  33. theorem OAI.SK.gaussian_exp_integrable line 264
  34. theorem OAI.SK.hamiltonian_exp_integral line 271
  35. theorem OAI.SK.hamiltonian_add_exp_integral line 279