OAI/Geometry/SmoothYau/Smoothness/ThreeRankNormedSpace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.inChart_deriv_curve line 16
2. lemma OAI.YauCounterexamples.linear_prod_surjective_of_directions line 30
3. def OAI.YauCounterexamples.threeMeridianEnergy line 44
4. lemma OAI.YauCounterexamples.threeMeridianEnergy_smooth line 47
5. lemma OAI.YauCounterexamples.threeMeridianEnergy_zero line 50
6. lemma OAI.YauCounterexamples.threeMeridianEnergy_right line 55
7. lemma OAI.YauCounterexamples.exists_threeMeridianEnergy_deriv line 60
8. lemma OAI.YauCounterexamples.threeMeridian_circle_deriv_ne line 75
9. lemma OAI.YauCounterexamples.exists_threeCoupled_gradient_rank line 86