OAI/Geometry/SmoothYau/Smoothness/SecondDerivNonposLocalMax.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.second_deriv_nonpos_of_localMax line 16
2. lemma OAI.YauCounterexamples.matrix_contraction_nonpos line 28
3. lemma OAI.YauCounterexamples.second_fderiv_diag_nonpos line 66
4. lemma OAI.YauCounterexamples.localMax_hessian_contraction line 98