OAI/Analysis/HardSphere/Geometry/FirstVariation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HardSphere.IsGroundVector.first_variation line 13
  2. theorem OAI.HardSphere.IsGroundVector.rayleigh line 26
  3. lemma OAI.HardSphere.torusDistance_comm line 35
  4. lemma OAI.HardSphere.allowed_iff_ne line 39
  5. lemma OAI.HardSphere.allowed_permute line 49
  6. def OAI.HardSphere.permuteLift line 59
  7. lemma OAI.HardSphere.permuteLift_direction line 70
  8. lemma OAI.HardSphere.coordDerivative_permute line 80
  9. def OAI.HardSphere.SmoothTest.permute line 93
  10. lemma OAI.HardSphere.continuous_permutationPullback_jet line 114
  11. def OAI.HardSphere.permutationJet line 123
  12. lemma OAI.HardSphere.SmoothTest.jet_permute line 133
  13. lemma OAI.HardSphere.permutationJet_mem_domain line 151
  14. lemma OAI.HardSphere.energy_permutationJet line 158