OAI/Geometry/WeakHessian/Entropy/LocalGradientParallelogram.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.LocalSobolev.neg line 52
  2. lemma OAI.WeakHessian.LocalSobolev.sub line 56
  3. lemma OAI.WeakHessian.weakGradient_neg line 61
  4. lemma OAI.WeakHessian.gamma_comm line 65
  5. lemma OAI.WeakHessian.gamma_zero_left line 72
  6. def OAI.WeakHessian.LocalGradientParallelogram line 76
  7. lemma OAI.WeakHessian.gamma_add_left line 82
  8. lemma OAI.WeakHessian.gamma_add_right line 92
  9. lemma OAI.WeakHessian.gamma_neg_left line 99
  10. lemma OAI.WeakHessian.gamma_sub_left line 107
  11. lemma OAI.WeakHessian.weakGradient_dist_le line 113
  12. lemma OAI.WeakHessian.weakGradient_const_mul_add_tendsto line 124
  13. lemma OAI.WeakHessian.gamma_const_mul_tendsto line 142