OAI/Probability/SKFluctuations/Spin.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

Spin.

  1. abbrev OAI.SKFluctuations.Spin line 21
  2. abbrev OAI.SKFluctuations.Edge line 22
  3. abbrev OAI.SKFluctuations.Disorder line 23
  4. def OAI.SKFluctuations.spinValue line 25
  5. def OAI.SKFluctuations.disorderLaw line 27
  6. def OAI.SKFluctuations.hamiltonian line 30
  7. def OAI.SKFluctuations.partitionFunction line 34
  8. def OAI.SKFluctuations.freeEnergy line 37
  9. def OAI.SKFluctuations.meanFreeEnergy line 40
  10. def OAI.SKFluctuations.freeEnergyVariance line 43
  11. def OAI.SKFluctuations.freeEnergySD line 46
  12. def OAI.SKFluctuations.fluctuationEvent line 49
  13. instance OAI.SKFluctuations.disorderLaw_isProbability line 53
  14. theorem OAI.SKFluctuations.abs_spinValue line 57
  15. theorem OAI.SKFluctuations.card_spin line 60
  16. theorem OAI.SKFluctuations.prior_mass line 64
  17. theorem OAI.SKFluctuations.continuous_hamiltonian line 69
  18. theorem OAI.SKFluctuations.continuous_partitionFunction line 74
  19. theorem OAI.SKFluctuations.partitionFunction_pos line 82
  20. theorem OAI.SKFluctuations.continuous_freeEnergy line 87
  21. def OAI.SKFluctuations.disorderSize line 92
  22. theorem OAI.SKFluctuations.abs_hamiltonian_le line 95
  23. theorem OAI.SKFluctuations.partitionFunction_le line 106
  24. theorem OAI.SKFluctuations.le_partitionFunction line 118
  25. theorem OAI.SKFluctuations.abs_freeEnergy_le line 131
  26. theorem OAI.SKFluctuations.memLp_disorderSize line 140
  27. theorem OAI.SKFluctuations.memLp_freeEnergy line 148
  28. theorem OAI.SKFluctuations.integrable_freeEnergy line 155
  29. theorem OAI.SKFluctuations.freeEnergyVariance_eq_integral line 159
  30. theorem OAI.SKFluctuations.freeEnergyVariance_nonneg line 164
  31. theorem OAI.SKFluctuations.integrable_exp_mul_abs_gaussian line 168
  32. theorem OAI.SKFluctuations.integrable_exp_disorderSize line 183
  33. theorem OAI.SKFluctuations.integrable_exp_freeEnergy line 194
  34. def OAI.SKFluctuations.finiteLogSumExp line 210
  35. theorem OAI.SKFluctuations.finite_partition_pos line 213
  36. theorem OAI.SKFluctuations.normalized_exp_sum line 217
  37. theorem OAI.SKFluctuations.convex_finiteLogSumExp line 226
  38. theorem OAI.SKFluctuations.hamiltonian_add line 257
  39. theorem OAI.SKFluctuations.hamiltonian_smul line 262
  40. theorem OAI.SKFluctuations.convex_freeEnergy line 269
  41. def OAI.SKFluctuations.completionVariance line 284
  42. def OAI.SKFluctuations.completedLaw line 286
  43. def OAI.SKFluctuations.completedFreeEnergy line 289
  44. instance OAI.SKFluctuations.completedLaw_isProbability line 292
  45. theorem OAI.SKFluctuations.memLp_completedFreeEnergy line 297
  46. theorem OAI.SKFluctuations.integrable_completedFreeEnergy line 302
  47. theorem OAI.SKFluctuations.mean_completedFreeEnergy line 306
  48. theorem OAI.SKFluctuations.variance_completedFreeEnergy line 316
  49. theorem OAI.SKFluctuations.mgf_completedFreeEnergy line 325
  50. theorem OAI.SKFluctuations.integrable_exp_completedFreeEnergy line 338
  51. def OAI.SKFluctuations.laplaceTransform line 346
  52. def OAI.SKFluctuations.completedLaplaceTransform line 349
  53. theorem OAI.SKFluctuations.laplaceTransform_eq line 353
  54. theorem OAI.SKFluctuations.completedLaplaceTransform_eq line 360
  55. def OAI.SKFluctuations.centeredLogLaplace line 372
  56. def OAI.SKFluctuations.completedCenteredLogLaplace line 375
  57. theorem OAI.SKFluctuations.laplaceTransform_pos line 378
  58. theorem OAI.SKFluctuations.completedCenteredLogLaplace_eq line 384
  59. def OAI.SKFluctuations.centeredFreeEnergy line 391
  60. theorem OAI.SKFluctuations.integral_centeredFreeEnergy line 394
  61. theorem OAI.SKFluctuations.integrable_centeredFreeEnergy line 400
  62. theorem OAI.SKFluctuations.integrable_exp_centeredFreeEnergy line 404
  63. theorem OAI.SKFluctuations.one_le_laplaceTransform line 409
  64. theorem OAI.SKFluctuations.centeredLogLaplace_nonneg line 420
  65. theorem OAI.SKFluctuations.integrableExpSet_centeredFreeEnergy line 424
  66. theorem OAI.SKFluctuations.centeredLogLaplace_eq_cgf line 430
  67. theorem OAI.SKFluctuations.analyticAt_centeredLogLaplace line 435
  68. theorem OAI.SKFluctuations.exists_centeredLogLaplace_eq_secondDeriv line 443
  69. def OAI.SKFluctuations.PositiveLaplaceWindow line 453
  70. def OAI.SKFluctuations.spinGauge line 462
  71. theorem OAI.SKFluctuations.spinValue_beq line 474
  72. theorem OAI.SKFluctuations.spinValue_sq line 478
  73. def OAI.SKFluctuations.gaugeDisorder line 482
  74. theorem OAI.SKFluctuations.hamiltonian_gauge line 485
  75. theorem OAI.SKFluctuations.partitionFunction_gauge line 495
  76. theorem OAI.SKFluctuations.freeEnergy_gauge line 502
  77. theorem OAI.SKFluctuations.spinGauge_transitive line 506
  78. theorem OAI.SKFluctuations.gaussianReal_map_spinSigns line 513
  79. theorem OAI.SKFluctuations.measurePreserving_gaugeDisorder line 520
  80. def OAI.SKFluctuations.MainFluctuationStatement line 531