OAI/Probability/SKBarriers/SpinGlass/DisorderPairs.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.disorderPairLaw line 12
  2. instance OAI.SK.disorderLaw_isGaussian line 15
  3. instance OAI.SK.disorderPairLaw_probability line 20
  4. theorem OAI.SK.disorderPair_fst_law line 24
  5. theorem OAI.SK.disorderPair_snd_law line 29
  6. theorem OAI.SK.disorderPair_independent line 34
  7. theorem OAI.SK.disorderPair_gaussian line 41
  8. theorem OAI.SK.disorderPair_fst_coordinate_law line 46
  9. theorem OAI.SK.disorderPair_snd_coordinate_law line 51
  10. theorem OAI.SK.disorderPair_fst_covariance line 56
  11. theorem OAI.SK.disorderPair_snd_covariance line 64
  12. theorem OAI.SK.disorderPair_cross_covariance line 72
  13. theorem OAI.SK.covariance_linear_combination line 80
  14. def OAI.SK.mixDisorder line 96
  15. def OAI.SK.mixDisorderCLM line 99
  16. theorem OAI.SK.mixDisorderCLM_apply line 103
  17. theorem OAI.SK.mixDisorder_gaussian line 106
  18. theorem OAI.SK.mixDisorder_mean line 110
  19. theorem OAI.SK.mixDisorder_covariance line 121
  20. theorem OAI.SK.mixDisorder_coordinate_law line 136
  21. theorem OAI.SK.mixDisorder_law line 148
  22. def OAI.SK.rotateDisorder line 155
  23. def OAI.SK.rotateDisorderCLM line 160
  24. theorem OAI.SK.rotateDisorderCLM_apply line 165
  25. theorem OAI.SK.rotateDisorder_gaussian line 168
  26. theorem OAI.SK.rotateDisorder_law line 172
  27. def OAI.SK.directionalEnergy line 184
  28. theorem OAI.SK.directionalEnergy_exp_le line 187
  29. theorem OAI.SK.continuous_hamiltonian line 197
  30. theorem OAI.SK.continuous_partition line 202
  31. theorem OAI.SK.continuous_gibbs line 208
  32. theorem OAI.SK.gibbs_le_one line 214
  33. theorem OAI.SK.gibbs_integrable line 219
  34. theorem OAI.SK.continuous_directionalEnergy line 225
  35. theorem OAI.SK.directionalEnergy_exp_integrable line 232
  36. theorem OAI.SK.directionalEnergy_exp_integral_le line 247
  37. theorem OAI.SK.directionalEnergy_pair_exp_integrable line 264
  38. theorem OAI.SK.directionalEnergy_pair_exp_integral_le line 281
  39. theorem OAI.SK.hamiltonian_mix line 293