OAI/Analysis/BiholderTransport/Contact/MiddleExclusion.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.neg_cost_ray_lipschitz line 22
  2. def OAI.WeakMTWTransport.rayMountainDifference line 33
  3. lemma OAI.WeakMTWTransport.rayMountainDifference_lipschitzOn line 38
  4. lemma OAI.WeakMTWTransport.rayMountainDifference_hasDerivAt line 50
  5. lemma OAI.WeakMTWTransport.middle_mountain_barrier line 64
  6. def OAI.WeakMTWTransport.templateEps line 91
  7. def OAI.WeakMTWTransport.centerGamma line 93
  8. def OAI.WeakMTWTransport.centerTemplate line 95
  9. lemma OAI.WeakMTWTransport.templateEps_eq line 98
  10. lemma OAI.WeakMTWTransport.centerGamma_pos line 99
  11. lemma OAI.WeakMTWTransport.centerTemplate_smooth line 103
  12. lemma OAI.WeakMTWTransport.centerTemplate_bounds line 110
  13. lemma OAI.WeakMTWTransport.centerTemplate_left line 121
  14. lemma OAI.WeakMTWTransport.centerTemplate_right line 139
  15. lemma OAI.WeakMTWTransport.hasDerivAt_centerTemplate line 148
  16. lemma OAI.WeakMTWTransport.centerTemplate_deriv_neg line 164
  17. def OAI.WeakMTWTransport.outerVelocity line 171
  18. def OAI.WeakMTWTransport.outerPrimitive line 179
  19. def OAI.WeakMTWTransport.outerTemplate line 182
  20. lemma OAI.WeakMTWTransport.outerVelocity_smooth line 186
  21. lemma OAI.WeakMTWTransport.outerVelocity_zero_left line 190
  22. lemma OAI.WeakMTWTransport.outerVelocity_zero_right line 195
  23. lemma OAI.WeakMTWTransport.outerVelocity_core line 202