OAI/Probability/SKBarriers/SpinGlass/LogPartition.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SK.logPartition line 12
  2. theorem OAI.SK.continuous_logPartition line 14
  3. theorem OAI.SK.logPartition_hasDerivAt line 18
  4. theorem OAI.SK.continuous_rotateDisorder line 36
  5. theorem OAI.SK.rotation_logPartition_hasDerivAt line 41
  6. theorem OAI.SK.continuous_rotation_path line 57
  7. theorem OAI.SK.continuous_rotation_energy line 62
  8. theorem OAI.SK.rotation_logPartition_integral line 67
  9. def OAI.SK.unitIntervalLaw line 82
  10. instance OAI.SK.unitIntervalLaw_probability line 84
  11. theorem OAI.SK.continuous_unitInterval_integrable line 88
  12. theorem OAI.SK.unitInterval_integral line 92
  13. theorem OAI.SK.rotation_exp_jensen line 97
  14. theorem OAI.SK.rotated_directionalEnergy_exp_integrable line 116
  15. theorem OAI.SK.rotated_directionalEnergy_exp_integral_le line 123
  16. def OAI.SK.rotationIntegrand line 139
  17. theorem OAI.SK.continuous_rotationIntegrand line 143
  18. theorem OAI.SK.rotationIntegrand_integrable line 158
  19. theorem OAI.SK.rotation_exp_integrable line 177
  20. theorem OAI.SK.rotation_exp_integral_le line 195
  21. theorem OAI.SK.rotateDisorder_pi_div_two_fst line 230
  22. theorem OAI.SK.logPartition_difference_exp_integrable line 235
  23. theorem OAI.SK.logPartition_exp_integrable line 241
  24. theorem OAI.SK.logPartition_integrable line 252
  25. theorem OAI.SK.logPartition_centered_exp_jensen line 269
  26. theorem OAI.SK.logPartition_centered_exp_integrable line 290
  27. theorem OAI.SK.logPartition_centered_exp_integral_le line 302