OAI/Geometry/QuadricBundles/DiskHessian.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadricCounterexample._root_.OAI.IsLocalMax.second_deriv_nonpos line 11
2. lemma OAI.QuadricCounterexample.deriv_affine_eventually line 25
3. lemma OAI.QuadricCounterexample.hasDerivAt_fderiv_affine line 40
4. lemma OAI.QuadricCounterexample.second_deriv_affine line 56
5. lemma OAI.QuadricCounterexample._root_.OAI.IsLocalMax.hessian_nonpos line 63
6. def OAI.QuadricCounterexample.complexLaplacian line 77
7. lemma OAI.QuadricCounterexample._root_.OAI.IsLocalMax.complexLaplacian_nonpos line 81
8. lemma OAI.QuadricCounterexample.rotated_hessian_trace line 85
9. lemma OAI.QuadricCounterexample.complexLaplacian_norm_sq line 98
10. lemma OAI.QuadricCounterexample.hessian_add line 112
11. lemma OAI.QuadricCounterexample.complexLaplacian_add line 124
12. lemma OAI.QuadricCounterexample.hessian_smul line 130
13. lemma OAI.QuadricCounterexample.complexLaplacian_smul line 140
14. lemma OAI.QuadricCounterexample.C2_le_boundary line 146
15. lemma OAI.QuadricCounterexample.compactParameter_integrable line 211
16. lemma OAI.QuadricCounterexample.compactParameter_continuousAtIntegral line 219
17. lemma OAI.QuadricCounterexample.compactParameter_hasFDerivAtIntegral line 236
18. lemma OAI.QuadricCounterexample.compactParameter_secondFDerivIntegral line 255
19. lemma OAI.QuadricCounterexample.compactParameter_contDiffOn_one_Integral line 269
20. lemma OAI.QuadricCounterexample.compactParameter_contDiffOn_two_Integral line 284