OAI/MathematicalPhysics/CriticalSK/HighTemperature.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CriticalSK.spinValue_abs line 18
  2. lemma OAI.CriticalSK.hamiltonian_gaussianLinear line 20
  3. lemma OAI.CriticalSK.edge_card_le_sq line 27
  4. lemma OAI.CriticalSK.hamiltonian_exp_moment line 30
  5. lemma OAI.CriticalSK.hamiltonian_one_sided_tail line 57
  6. lemma OAI.CriticalSK.hamiltonian_abs_tail line 71
  7. lemma OAI.CriticalSK.spin_card_le_exp line 84
  8. lemma OAI.CriticalSK.maximum_energy_tail line 90
  9. lemma OAI.CriticalSK.maximum_energy_tendsto line 102
  10. lemma OAI.CriticalSK.polynomial_exp_eventually_le line 118
  11. lemma OAI.CriticalSK.finite_tempered_mixing line 129
  12. lemma OAI.CriticalSK.tempered_mixing_eventual_implication line 154
  13. lemma OAI.CriticalSK.temperature_close_to_one line 170
  14. lemma OAI.CriticalSK.fiberMass_continuous line 182
  15. lemma OAI.CriticalSK.siteKernel_continuous line 191
  16. lemma OAI.CriticalSK.mean_continuous line 198
  17. lemma OAI.CriticalSK.variance_continuous line 202
  18. lemma OAI.CriticalSK.dirichlet_continuous line 209
  19. def OAI.CriticalSK.poincareEvent line 220
  20. lemma OAI.CriticalSK.poincareEvent_closed line 223
  21. lemma OAI.CriticalSK.tempered_mixing_probability_lower line 233
  22. def OAI.CriticalSK.mixingReductionError line 258
  23. def OAI.CriticalSK.twoClockMixingEvent line 263
  24. lemma OAI.CriticalSK.mixingReductionError_tendsto line 269
  25. lemma OAI.CriticalSK.mixingGapReduction_lower line 281