OAI/Geometry/WeakHessian/Sobolev/GradientPairSum.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakHessian.weakGradient_triangularFold_of_measurable line 51
  2. lemma OAI.WeakHessian.weakGradient_triangularFold line 78
  3. def OAI.WeakHessian.gradientPairSum line 89
  4. lemma OAI.WeakHessian.gradientPairSum_symm line 94
  5. lemma OAI.WeakHessian.gradientPairSum_neg_left line 103
  6. lemma OAI.WeakHessian.gradientPairSum_add_const_left line 114
  7. lemma OAI.WeakHessian.gradientPairSum_locality_left line 127
  8. lemma OAI.WeakHessian.gradientPairSum_fold_left_of_measurable line 141
  9. lemma OAI.WeakHessian.gradientPairSum_congr_ae line 172
  10. lemma OAI.WeakHessian.gradientPairSum_fold_left line 181
  11. lemma OAI.WeakHessian.gradientPairSum_fold line 191