OAI/Geometry/WeakHessian/LocalBounds/DyadicTimes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.continuous_halfTime line 39
  2. lemma OAI.WeakHessian.continuous_rightTime line 41
  3. lemma OAI.WeakHessian.dist_halfTime line 44
  4. lemma OAI.WeakHessian.dist_rightTime line 47
  5. lemma OAI.WeakHessian.halfTime_zero line 51
  6. lemma OAI.WeakHessian.rightTime_one line 53
  7. lemma OAI.WeakHessian.halfTime_one_eq_rightTime_zero line 55
  8. def OAI.WeakHessian.dyadicTimes line 58
  9. lemma OAI.WeakHessian.zero_mem_dyadicTimes line 62
  10. lemma OAI.WeakHessian.one_mem_dyadicTimes line 66
  11. lemma OAI.WeakHessian.monotone_dyadicTimes line 71
  12. lemma OAI.WeakHessian.exists_dyadicTime_dist_le line 85
  13. lemma OAI.WeakHessian.dense_dyadicTimes line 107