OAI/MathematicalPhysics/CriticalSK/Cavity.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalSK.flipSite line 18
  2. lemma OAI.CriticalSK.flipSite_apply_self line 20
  3. lemma OAI.CriticalSK.flipSite_apply_ne line 22
  4. lemma OAI.CriticalSK.flipSite_involutive line 24
  5. lemma OAI.CriticalSK.flipSite_ne line 30
  6. def OAI.CriticalSK.flipSiteEquiv line 36
  7. lemma OAI.CriticalSK.sameExcept_flipSite line 42
  8. lemma OAI.CriticalSK.sameExcept_two line 46
  9. lemma OAI.CriticalSK.sum_sameExcept line 68
  10. def OAI.CriticalSK.incidentCoeff line 79
  11. def OAI.CriticalSK.localField line 82
  12. def OAI.CriticalSK.deleteDisorder line 85
  13. lemma OAI.CriticalSK.incidentCoeff_fiber line 88
  14. lemma OAI.CriticalSK.localField_fiber line 97
  15. lemma OAI.CriticalSK.delete_hamiltonian_fiber line 101
  16. lemma OAI.CriticalSK.hamiltonian_cavity line 110
  17. lemma OAI.CriticalSK.gibbs_delete_fiber line 122
  18. lemma OAI.CriticalSK.cavity_exp_pair line 126
  19. def OAI.CriticalSK.cavityNormalization line 134
  20. lemma OAI.CriticalSK.cavityNormalization_ge_one line 137
  21. lemma OAI.CriticalSK.partition_cavity line 141
  22. lemma OAI.CriticalSK.gibbs_cavity line 156
  23. lemma OAI.CriticalSK.gibbs_cavity_pair line 161
  24. lemma OAI.CriticalSK.mean_cavity_even line 171
  25. lemma OAI.CriticalSK.siteAverage_two line 183
  26. lemma OAI.CriticalSK.siteAverage_spin line 193
  27. def OAI.CriticalSK.alphaSite line 204
  28. lemma OAI.CriticalSK.alphaSite_pos line 206
  29. lemma OAI.CriticalSK.mean_mul_mean_inv line 218
  30. lemma OAI.CriticalSK.alphaSite_cavity line 227
  31. lemma OAI.CriticalSK.alphaSite_normalization line 235
  32. lemma OAI.CriticalSK.one_sub_tanh_sq line 243
  33. lemma OAI.CriticalSK.site_spin_variance line 249
  34. lemma OAI.CriticalSK.siteAverage_const_mul line 261
  35. lemma OAI.CriticalSK.siteAverage_linear_residual line 269
  36. lemma OAI.CriticalSK.dirichlet_linear_eq line 278
  37. lemma OAI.CriticalSK.dirichlet_linear_pos line 286
  38. lemma OAI.CriticalSK.mean_delete_le line 293
  39. def OAI.CriticalSK.cavityOverlapCoord line 301
  40. def OAI.CriticalSK.cavityOverlap line 304
  41. lemma OAI.CriticalSK.cavityOverlapCoord_eq line 307
  42. lemma OAI.CriticalSK.cavityOverlapCoord_fiber_left line 315
  43. lemma OAI.CriticalSK.cavityOverlapCoord_comm line 323
  44. lemma OAI.CriticalSK.cavityOverlap_nonneg line 327
  45. lemma OAI.CriticalSK.cavityOverlap_compare line 330
  46. def OAI.CriticalSK.touches line 364
  47. instance OAI.CriticalSK.(instance at line 366) line 366
  48. abbrev OAI.CriticalSK.Incident line 368
  49. abbrev OAI.CriticalSK.Nonincident line 370
  50. def OAI.CriticalSK.edgeOfOther line 372
  51. lemma OAI.CriticalSK.edgeOfOther_touches line 375
  52. def OAI.CriticalSK.otherEnd line 379
  53. lemma OAI.CriticalSK.otherEnd_ne line 382
  54. def OAI.CriticalSK.incidentOtherEquiv line 387
  55. lemma OAI.CriticalSK.incidentCoeff_other line 403
  56. lemma OAI.CriticalSK.sum_incident_other line 411
  57. lemma OAI.CriticalSK.incident_coeff_square line 417
  58. lemma OAI.CriticalSK.incident_coeff_product line 425
  59. def OAI.CriticalSK.cavitySplit line 432
  60. def OAI.CriticalSK.incidentLaw line 435
  61. def OAI.CriticalSK.nonincidentLaw line 438
  62. instance OAI.CriticalSK.(instance at line 441) line 441
  63. instance OAI.CriticalSK.(instance at line 443) line 443
  64. lemma OAI.CriticalSK.cavitySplit_preserving line 445
  65. lemma OAI.CriticalSK.cavityJoin_apply_incident line 449
  66. lemma OAI.CriticalSK.cavityJoin_apply_nonincident line 453
  67. lemma OAI.CriticalSK.delete_cavityJoin line 457
  68. lemma OAI.CriticalSK.localField_cavityJoin line 468