OAI/Probability/SKGap/Terminal/Spin.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGapCutoff.Spin line 12
  2. abbrev OAI.SKGapCutoff.Interaction line 13
  3. def OAI.SKGapCutoff.spin line 15
  4. def OAI.SKGapCutoff.replace line 17
  5. def OAI.SKGapCutoff.halfDiff line 20
  6. def OAI.SKGapCutoff.field line 23
  7. def OAI.SKGapCutoff.mean line 26
  8. def OAI.SKGapCutoff.generator line 29
  9. def OAI.SKGapCutoff.gradientGenerator line 32
  10. theorem OAI.SKGapCutoff.replace_same line 39
  11. theorem OAI.SKGapCutoff.replace_replace line 43
  12. theorem OAI.SKGapCutoff.replace_self line 47
  13. theorem OAI.SKGapCutoff.replace_comm line 51
  14. theorem OAI.SKGapCutoff.halfDiff_replace line 55
  15. theorem OAI.SKGapCutoff.halfDiff_self line 59
  16. theorem OAI.SKGapCutoff.halfDiff_mul line 63
  17. theorem OAI.SKGapCutoff.halfDiff_comm line 76
  18. theorem OAI.SKGapCutoff.halfDiff_const line 86
  19. theorem OAI.SKGapCutoff.halfDiff_sub line 90
  20. theorem OAI.SKGapCutoff.halfDiff_sum line 95
  21. theorem OAI.SKGapCutoff.halfDiff_spin line 100
  22. theorem OAI.SKGapCutoff.halfDiff_generator line 107
  23. abbrev OAI.SKGapCutoff.Observables line 123
  24. abbrev OAI.SKGapCutoff.VectorFields line 124
  25. def OAI.SKGapCutoff.gradientLM line 126
  26. def OAI.SKGapCutoff.generatorLM line 137
  27. def OAI.SKGapCutoff.gradientGeneratorLM line 153
  28. def OAI.SKGapCutoff.gradientCLM line 182
  29. def OAI.SKGapCutoff.generatorCLM line 185
  30. def OAI.SKGapCutoff.gradientGeneratorCLM line 188
  31. def OAI.SKGapCutoff.semigroup line 192
  32. def OAI.SKGapCutoff.gradientSemigroup line 195
  33. theorem OAI.SKGapCutoff.exp_intertwine line 199
  34. theorem OAI.SKGapCutoff.halfDiff_semigroup line 224
  35. def OAI.SKGapCutoff.energy line 239
  36. def OAI.SKGapCutoff.partition line 242
  37. def OAI.SKGapCutoff.gibbs line 245
  38. def OAI.SKGapCutoff.attemptLM line 248
  39. def OAI.SKGapCutoff.continuousKernel line 252
  40. def OAI.SKGapCutoff.discreteKernel line 255
  41. def OAI.SKGapCutoff.totalVariation line 258
  42. def OAI.SKGapCutoff.worstContinuous line 261
  43. def OAI.SKGapCutoff.worstDiscrete line 265
  44. abbrev OAI.SKGapCutoff.GaussianCoordinates line 269
  45. def OAI.SKGapCutoff.disorderLaw line 271
  46. def OAI.SKGapCutoff.sampledInteraction line 276
  47. def OAI.SKGapCutoff.cutoffTime line 279
  48. def OAI.SKGapCutoff.DisorderLimit line 281
  49. def OAI.SKGapCutoff.CutoffAtRate line 287
  50. theorem OAI.SKGapCutoff.sampledInteraction_diag line 296
  51. theorem OAI.SKGapCutoff.sampledInteraction_symm line 299
  52. theorem OAI.SKGapCutoff.partition_pos line 305
  53. theorem OAI.SKGapCutoff.gibbs_pos line 308
  54. theorem OAI.SKGapCutoff.gibbs_sum line 311
  55. def OAI.SKGapCutoff.siteRefresh line 315
  56. theorem OAI.SKGapCutoff.generator_siteRefresh line 320
  57. theorem OAI.SKGapCutoff.attempt_apply_of_pos line 333
  58. theorem OAI.SKGapCutoff.generator_const line 343
  59. theorem OAI.SKGapCutoff.siteRefresh_const line 347
  60. theorem OAI.SKGapCutoff.attempt_const line 352
  61. theorem OAI.SKGapCutoff.attempt_pow_const line 358
  62. theorem OAI.SKGapCutoff.siteRefresh_nonneg line 364
  63. theorem OAI.SKGapCutoff.attempt_nonneg line 372
  64. theorem OAI.SKGapCutoff.attempt_pow_nonneg line 381
  65. theorem OAI.SKGapCutoff.discreteKernel_nonneg line 389
  66. theorem OAI.SKGapCutoff.discreteKernel_sum line 393