OAI/Analysis/HardSphere/Geometry/SqTwiceSqAbs.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.sq_le_twice_sq_of_abs_le line 22
  2. lemma OAI.HardSphere.closeAmplitude_sum_sq line 30
  3. lemma OAI.HardSphere.localCloseRoot_difference_sq line 48
  4. theorem OAI.HardSphere.localCloseRoot_difference line 58
  5. abbrev OAI.HardSphere.EuclideanConfiguration line 79
  6. def OAI.HardSphere.euclideanProject line 81
  7. lemma OAI.HardSphere.euclideanProject_continuous line 84
  8. lemma OAI.HardSphere.euclideanProject_sub line 88
  9. lemma OAI.HardSphere.euclideanProject_surjective line 93
  10. lemma OAI.HardSphere.euclideanProject_total_sq line 99
  11. lemma OAI.HardSphere.closeAmplitude_continuous line 118
  12. lemma OAI.HardSphere.localCloseRoot_continuous line 129
  13. theorem OAI.HardSphere.localCloseRoot_euclidean_lipschitz line 134