OAI/Probability/DilutedSpin/PhysicalIndex.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DilutedSpinGlass.abs_spin line 11
  2. theorem OAI.DilutedSpinGlass.sum_exp_pos line 13
  3. theorem OAI.DilutedSpinGlass.logSumExp_stability line 18
  4. theorem OAI.DilutedSpinGlass.logWeight_bound line 31
  5. theorem OAI.DilutedSpinGlass.logPartition_bound line 41
  6. theorem OAI.DilutedSpinGlass.logWeight_stability line 53
  7. theorem OAI.DilutedSpinGlass.logPartition_stability line 70
  8. def OAI.DilutedSpinGlass.indexAverage line 76
  9. theorem OAI.DilutedSpinGlass.indexAverage_bound line 81
  10. theorem OAI.DilutedSpinGlass.continuous_logPartition line 101
  11. theorem OAI.DilutedSpinGlass.continuous_indexAverage line 111