OAI/Probability/ContinuumTransition/PairEnergy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ContinuumTemperature.ereal_sum_eq_top_of_exists line 12
  2. theorem OAI.ContinuumTemperature.energy_eq_top_iff line 27
  3. def OAI.ContinuumTemperature.realPairEnergy line 52
  4. theorem OAI.ContinuumTemperature.realPairEnergy_eq_ordered line 57
  5. def OAI.ContinuumTemperature.symmetricWeight line 87
  6. theorem OAI.ContinuumTemperature.boltzmann_eq_symmetricWeight line 91
  7. theorem OAI.ContinuumTemperature.realPairEnergy_relabel line 99
  8. theorem OAI.ContinuumTemperature.symmetricWeight_relabel line 110
  9. theorem OAI.ContinuumTemperature.symmetric_matrix_split line 124
  10. theorem OAI.ContinuumTemperature.realPairEnergy_split line 146
  11. theorem OAI.ContinuumTemperature.symmetricWeight_nonneg line 165
  12. theorem OAI.ContinuumTemperature.symmetricWeight_separated line 172
  13. theorem OAI.ContinuumTemperature.realPairEnergy_translate line 202
  14. theorem OAI.ContinuumTemperature.symmetricWeight_translate line 208