OAI/Analysis/HardSphere/Geometry/InjectiveNear.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.exists_injective_near line 22
  2. lemma OAI.HardSphere.dense_injective_configurations line 59
  3. lemma OAI.HardSphere.torus_nontrivial line 67
  4. lemma OAI.HardSphere.torusDistance_continuous_pair line 77
  5. lemma OAI.HardSphere.nearestDifference_continuous line 84
  6. lemma OAI.HardSphere.torusMotion_continuous line 92
  7. theorem OAI.HardSphere.nearestParticleDistance_sum_sq_all line 102
  8. def OAI.HardSphere.closeRamp line 120
  9. lemma OAI.HardSphere.closeRamp_nonneg line 122
  10. lemma OAI.HardSphere.closeRamp_le_one line 123
  11. lemma OAI.HardSphere.closeRamp_one line 124
  12. lemma OAI.HardSphere.closeRamp_zero line 125
  13. lemma OAI.HardSphere.closeRamp_lipschitz line 127
  14. lemma OAI.HardSphere.closeRamp_sub_le line 130
  15. def OAI.HardSphere.closeAmplitude line 135
  16. def OAI.HardSphere.localCloseRoot line 138
  17. def OAI.HardSphere.localCloseSmoothCount line 141
  18. lemma OAI.HardSphere.localCloseRoot_sq line 144
  19. lemma OAI.HardSphere.closeAmplitude_nonneg line 148
  20. lemma OAI.HardSphere.closeAmplitude_le_one line 150
  21. lemma OAI.HardSphere.closeAmplitude_one line 155
  22. lemma OAI.HardSphere.closeAmplitude_zero_of_far line 162
  23. lemma OAI.HardSphere.closeAmplitude_zero_of_isolated line 167
  24. lemma OAI.HardSphere.torusDistance_sub_le line 173
  25. lemma OAI.HardSphere.unit_product_sub_le line 178
  26. lemma OAI.HardSphere.closeAmplitude_sub_le line 189