OAI/Geometry/WeakHessian/Calculus/ControlNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.HasControlBound.dist_le_modulus line 36
2. lemma OAI.WeakHessian.isCompact_hasControlBound line 44
3. lemma OAI.WeakHessian.hasControlBound_of_forall_gt line 60
4. def OAI.WeakHessian.controlNorm line 96
5. lemma OAI.WeakHessian.controlNorm_le line 99
6. lemma OAI.WeakHessian.controlNorm_le_iff line 103
7. lemma OAI.WeakHessian.lowerSemicontinuous_controlNorm line 114
8. lemma OAI.WeakHessian.controlNorm_lt_top_iff line 125
9. lemma OAI.WeakHessian.controlNorm_finite_isAC2 line 133