OAI/Analysis/HardSphere/FormDomain/Basic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.coordDerivative_add line 11
  2. lemma OAI.HardSphere.coordDerivative_smul line 21
  3. lemma OAI.HardSphere.coordDerivative_zero line 29
  4. def OAI.HardSphere.SmoothTest.zero line 34
  5. def OAI.HardSphere.SmoothTest.add line 45
  6. def OAI.HardSphere.SmoothTest.smul line 57
  7. lemma OAI.HardSphere.SmoothTest.jet_zero line 69
  8. lemma OAI.HardSphere.SmoothTest.jet_add line 77
  9. lemma OAI.HardSphere.SmoothTest.jet_smul line 88
  10. def OAI.HardSphere.smoothGraph line 99
  11. def OAI.HardSphere.dirichletSubmodule line 109
  12. lemma OAI.HardSphere.mem_dirichletSubmodule line 112
  13. def OAI.HardSphere.permuteConfiguration line 115
  14. lemma OAI.HardSphere.measurePreserving_permute line 118
  15. def OAI.HardSphere.permutationPullback line 129
  16. lemma OAI.HardSphere.bosonic_iff_pullback line 135
  17. def OAI.HardSphere.bosonicSubmodule line 153
  18. lemma OAI.HardSphere.mem_bosonicSubmodule line 170
  19. def OAI.HardSphere.groundFormSubmodule line 178
  20. lemma OAI.HardSphere.mem_groundFormSubmodule line 182