OAI/Geometry/WeakHessian/LocalBounds/AffineTime.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakHessian.affineTime line 18
  2. theorem OAI.WeakHessian.affineTime_zero line 28
  3. theorem OAI.WeakHessian.affineTime_one line 32
  4. lemma OAI.WeakHessian.continuous_affineTime line 36
  5. def OAI.WeakHessian.restrictCurve line 40
  6. lemma OAI.WeakHessian.continuous_restrictCurve line 43
  7. lemma OAI.WeakHessian.restrictCurve_zero line 46
  8. lemma OAI.WeakHessian.restrictCurve_one line 49
  9. lemma OAI.WeakHessian.clampTime_of_mem line 52
  10. lemma OAI.WeakHessian.evalReal_restrictCurve line 56
  11. def OAI.WeakHessian.affineHomeomorph line 69
  12. lemma OAI.WeakHessian.affineHomeomorph_apply line 72
  13. lemma OAI.WeakHessian.metricSpeed_restrictCurve line 75
  14. lemma OAI.WeakHessian.map_affineHomeomorph_volume line 111
  15. lemma OAI.WeakHessian.affineHomeomorph_preimage_Icc line 119
  16. lemma OAI.WeakHessian.lintegral_affine_Icc line 125
  17. lemma OAI.WeakHessian.coe_affineTime line 139
  18. lemma OAI.WeakHessian.lintegral_scaled_affine_Icc line 144
  19. lemma OAI.WeakHessian.lintegral_scaled_sq_affine_Icc line 152
  20. lemma OAI.WeakHessian.IsAC2.restrictCurve line 165
  21. lemma OAI.WeakHessian.ae_metricSpeed_restrictCurve line 193
  22. lemma OAI.WeakHessian.kineticEnergy_restrictCurve line 201