OAI/Analysis/HardSphere/Geometry/FlattenLinear.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.flattenLinear line 22
  2. def OAI.HardSphere.euclideanFlatten line 27
  3. lemma OAI.HardSphere.euclideanFlatten_apply line 30
  4. lemma OAI.HardSphere.euclideanFlatten_project line 33
  5. lemma OAI.HardSphere.euclideanFlatten_single line 36
  6. lemma OAI.HardSphere.realEuclidean_lift_smooth line 42
  7. def OAI.HardSphere.realEuclideanMultiplier line 47
  8. lemma OAI.HardSphere.coordDerivative_real_euclidean line 51
  9. lemma OAI.HardSphere.clippedNearest_le line 74
  10. lemma OAI.HardSphere.clippedNearest_eq line 84
  11. lemma OAI.HardSphere.closeRamp_clipped line 91
  12. lemma OAI.HardSphere.far_from_near_separated line 101
  13. theorem OAI.HardSphere.closeAmplitude_away_eq line 108
  14. lemma OAI.HardSphere.localCloseSmoothCount_away_eq line 129
  15. def OAI.HardSphere.mollifiedCloseRoot line 144
  16. def OAI.HardSphere.mollifiedCloseCount line 148
  17. lemma OAI.HardSphere.mollifiedCloseRoot_nonneg line 152
  18. lemma OAI.HardSphere.mollifiedCloseRoot_smooth line 157
  19. lemma OAI.HardSphere.mollifiedCloseCount_smooth line 162
  20. lemma OAI.HardSphere.mollifiedCloseRoot_lipschitz line 167
  21. lemma OAI.HardSphere.mollifiedCloseRoot_approximation line 173
  22. lemma OAI.HardSphere.self_gradient_square_of_lipschitz line 179
  23. lemma OAI.HardSphere.mollifiedCloseCount_gradient line 193