OAI/Geometry/WeakHessian/Sobolev/Minimal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.exists_minimal line 47
  2. lemma OAI.WeakHessian.localSobolev_iff_exists_upperGradient line 106
  3. lemma OAI.WeakHessian.LocalSobolev.add line 115
  4. lemma OAI.WeakHessian.weakGradient_add_le line 121
  5. lemma OAI.WeakHessian.Sobolev.of_upperGradient line 128
  6. lemma OAI.WeakHessian.Sobolev.add line 138
  7. lemma OAI.WeakHessian.LocalSobolev.const_mul line 145
  8. lemma OAI.WeakHessian.Sobolev.const_mul line 155
  9. lemma OAI.WeakHessian.Sobolev.neg line 161
  10. lemma OAI.WeakHessian.Sobolev.sub line 164
  11. lemma OAI.WeakHessian.Sobolev.mul_bounded line 168