OAI/Geometry/PolarProducts/SmoothProfiles.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothProfiles.primitive line 12
  2. theorem OAI.SmoothProfiles.hasDerivAt_primitive line 14
  3. theorem OAI.SmoothProfiles.contDiff_primitive line 19
  4. theorem OAI.SmoothProfiles.primitive_zero line 24
  5. theorem OAI.SmoothProfiles.primitive_nonneg line 34
  6. theorem OAI.SmoothProfiles.primitive_mono line 40
  7. def OAI.SmoothProfiles.exteriorSlope line 45
  8. def OAI.SmoothProfiles.exterior line 46
  9. theorem OAI.SmoothProfiles.contDiff_exteriorSlope line 48
  10. theorem OAI.SmoothProfiles.contDiff_exterior line 51
  11. theorem OAI.SmoothProfiles.hasDerivAt_exterior line 54
  12. theorem OAI.SmoothProfiles.exteriorSlope_nonneg line 57
  13. theorem OAI.SmoothProfiles.exteriorSlope_le_one line 58
  14. theorem OAI.SmoothProfiles.exteriorSlope_zero line 59
  15. theorem OAI.SmoothProfiles.exteriorSlope_one line 61
  16. theorem OAI.SmoothProfiles.exterior_zero line 64
  17. theorem OAI.SmoothProfiles.exterior_nonneg line 67
  18. theorem OAI.SmoothProfiles.exterior_affine line 71
  19. theorem OAI.SmoothProfiles.exterior_lower line 85
  20. theorem OAI.SmoothProfiles.exterior_upper line 90
  21. theorem OAI.SmoothProfiles.primitive_zero_below line 100
  22. theorem OAI.SmoothProfiles.primitive_const_above line 108
  23. def OAI.SmoothProfiles.ballSlope line 120
  24. def OAI.SmoothProfiles.ballProfile line 122
  25. def OAI.SmoothProfiles.ballHeight line 123
  26. theorem OAI.SmoothProfiles.contDiff_ballSlope line 125
  27. theorem OAI.SmoothProfiles.contDiff_ballProfile line 129
  28. theorem OAI.SmoothProfiles.hasDerivAt_ballProfile line 132
  29. theorem OAI.SmoothProfiles.ballSlope_nonneg line 136
  30. theorem OAI.SmoothProfiles.ballSlope_le line 139
  31. theorem OAI.SmoothProfiles.ballSlope_zero_left line 148
  32. theorem OAI.SmoothProfiles.ballSlope_zero_right line 154
  33. theorem OAI.SmoothProfiles.ballSlope_middle line 161
  34. theorem OAI.SmoothProfiles.ballProfile_zero line 168
  35. theorem OAI.SmoothProfiles.ballProfile_plateau line 172
  36. theorem OAI.SmoothProfiles.ballProfile_nonneg line 177
  37. theorem OAI.SmoothProfiles.ballProfile_le_height line 182
  38. theorem OAI.SmoothProfiles.ballHeight_lower line 188
  39. theorem OAI.SmoothProfiles.exists_ball_parameters line 206