OAI/Probability/SKSupport/Support/NoTerminalPlateau.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ZeroTemperatureSK.terminal_plateau_q_lt_near_one line 15
  2. theorem OAI.ZeroTemperatureSK.minimizer_no_terminal_plateau line 53
  3. def OAI.ZeroTemperatureSK.spinHamiltonian line 91
  4. def OAI.ZeroTemperatureSK.spinDisorder line 95
  5. def OAI.ZeroTemperatureSK.expectedSKMaximum line 98
  6. def OAI.ZeroTemperatureSK.groundStateValue line 101
  7. def OAI.ZeroTemperatureSK.TerminalValueConclusion line 105
  8. def OAI.ZeroTemperatureSK.GaussianConclusion line 130