OAI/Geometry/WeakHessian/Entropy/GradientParallelogramDefect.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.lipschitz_inv_of_one_le line 52
2. def OAI.WeakHessian.gradientParallelogramDefect line 67
3. lemma OAI.WeakHessian.gradientParallelogramDefect_integrable line 72
4. lemma OAI.WeakHessian.integral_gradientParallelogramDefect_mul_sq line 78
5. lemma OAI.WeakHessian.weighted_parallelogram_defect_zero line 105