OAI/Analysis/HardSphere/Rescaling/PhysicalRescaling.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Rescaling.circle line 15
  2. def OAI.HardSphere.Rescaling.torus line 17
  3. def OAI.HardSphere.Rescaling.config line 18
  4. def OAI.HardSphere.Rescaling.configHomeo line 20
  5. lemma OAI.HardSphere.Rescaling.configHomeo_toFun line 24
  6. lemma OAI.HardSphere.Rescaling.config_continuous line 25
  7. lemma OAI.HardSphere.Rescaling.circle_project line 27
  8. lemma OAI.HardSphere.Rescaling.config_project line 31
  9. lemma OAI.HardSphere.Rescaling.circle_representative line 36
  10. lemma OAI.HardSphere.Rescaling.config_representative line 52
  11. lemma OAI.HardSphere.Rescaling.circle_distance line 57
  12. lemma OAI.HardSphere.Rescaling.torus_distance line 68
  13. lemma OAI.HardSphere.Rescaling.config_allowed line 75
  14. lemma OAI.HardSphere.Rescaling.volume_config line 83
  15. def OAI.HardSphere.Rescaling.jacobian line 90
  16. lemma OAI.HardSphere.Rescaling.jacobian_pos line 91
  17. instance OAI.HardSphere.Rescaling.config_haar line 95
  18. lemma OAI.HardSphere.Rescaling.config_preserving line 99