OAI/Geometry/SmoothYau/DifferentialEq/HmoDualNorm.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.positiveFormOn line 30
2. lemma OAI.YauCounterexamples.positiveFormOn_iff_unit line 34
3. theorem OAI.YauCounterexamples.isOpen_positiveFormOn line 52
4. def OAI.YauCounterexamples.hessianMargins line 83
5. theorem OAI.YauCounterexamples.isOpen_hessianMargins line 87
6. lemma OAI.YauCounterexamples.hessianMargins_of_strong line 103
7. lemma OAI.YauCounterexamples.hessianMargins_lower line 119
8. lemma OAI.YauCounterexamples.hessianMargins_plane line 129