OAI/Geometry/WeakHessian/Entropy/NonnegativeParallelogram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WeakHessianFunctional.NonnegativeParallelogram line 29
  2. def OAI.WeakHessianFunctional.energyPolar line 34
  3. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.zero line 39
  4. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.neg line 42
  5. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_comm line 45
  6. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_add_left line 49
  7. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_bound line 60
  8. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_smul_left line 69
  9. def OAI.WeakHessianFunctional.NonnegativeParallelogram.bilin line 88
  10. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_self line 96
  11. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_add line 103
  12. lemma OAI.WeakHessianFunctional.NonnegativeParallelogram.polar_cauchySchwarz line 109