OAI/Geometry/IsometricImmersion/Metrics/ModelProfile.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Model.squareTransition line 19
  2. theorem OAI.SmoothLocal.Model.squareTransition_contDiff line 21
  3. theorem OAI.SmoothLocal.Model.squareTransition_range line 24
  4. theorem OAI.SmoothLocal.Model.squareTransition_zero line 28
  5. theorem OAI.SmoothLocal.Model.squareTransition_one line 31
  6. theorem OAI.SmoothLocal.Model.squareTransition_monotone line 34
  7. theorem OAI.SmoothLocal.Model.squareTransition_deriv_nonneg line 38
  8. def OAI.SmoothLocal.Model.modelProfile line 41
  9. theorem OAI.SmoothLocal.Model.modelProfile_contDiff line 43
  10. theorem OAI.SmoothLocal.Model.modelProfile_even line 47
  11. theorem OAI.SmoothLocal.Model.modelProfile_plateau line 51
  12. theorem OAI.SmoothLocal.Model.modelProfile_bounds line 57
  13. theorem OAI.SmoothLocal.Model.modelProfile_pos_inside line 64
  14. theorem OAI.SmoothLocal.Model.modelProfile_eq_one_sub_sq line 68
  15. theorem OAI.SmoothLocal.Model.modelProfile_neg_outside line 72
  16. theorem OAI.SmoothLocal.Model.modelProfile_one line 77
  17. theorem OAI.SmoothLocal.Model.modelProfile_hasDerivAt line 81
  18. theorem OAI.SmoothLocal.Model.modelProfile_deriv line 90
  19. theorem OAI.SmoothLocal.Model.modelProfile_deriv_nonpos line 95
  20. theorem OAI.SmoothLocal.Model.modelProfile_deriv_one_neg line 103
  21. theorem OAI.SmoothLocal.Model.modelProfile_spec line 111
  22. def OAI.SmoothLocal.Model.modelCurvature line 123
  23. theorem OAI.SmoothLocal.Model.modelCurvature_contDiff line 126
  24. theorem OAI.SmoothLocal.Model.modelCurvature_central_square line 130
  25. theorem OAI.SmoothLocal.Model.modelCurvature_pos_lateral line 141
  26. theorem OAI.SmoothLocal.Model.modelCurvature_lateral_band_lower line 147
  27. theorem OAI.SmoothLocal.Model.modelCurvature_pos_transverse line 157
  28. theorem OAI.SmoothLocal.Model.modelCurvature_pos_lower_flow_band line 163
  29. theorem OAI.SmoothLocal.Model.modelCurvature_abs_le_model_square line 172