OAI/Probability/ClassicalON/CylindricalConfiguration.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.freeSpinReference line 14
  2. instance OAI.ClassicalON.freeSpinReference_isProbability line 15
  3. def OAI.ClassicalON.freeSpinEnergy line 18
  4. theorem OAI.ClassicalON.continuous_freeSpinEnergy line 22
  5. def OAI.ClassicalON.freeSpinMean line 25
  6. def OAI.ClassicalON.cylindricalConfiguration line 28
  7. theorem OAI.ClassicalON.continuous_cylindricalConfiguration line 32
  8. theorem OAI.ClassicalON.cylindricalConfiguration_preserves line 44
  9. theorem OAI.ClassicalON.integral_freeSpinReference_cylinder line 61
  10. theorem OAI.ClassicalON.cylindricalSpin_inner line 78
  11. theorem OAI.ClassicalON.cylindricalConfiguration_energy line 91