OAI/Geometry/SmoothYau/Smoothness/LpProductLinearMap.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.lpProductLinearMap line 13
2. lemma OAI.YauCounterexamples.lpProductLinearMap_apply line 17
3. def OAI.YauCounterexamples.lpProductFunction line 21
4. lemma OAI.YauCounterexamples.lpProductFunction_hasFDerivAt line 23
5. lemma OAI.YauCounterexamples.lpProductFunction_fderiv line 30
6. lemma OAI.YauCounterexamples.lpProductFunction_contDiff line 34
7. def OAI.YauCounterexamples.lpProductIsometry line 42
8. lemma OAI.YauCounterexamples.lpProductIsometry_apply line 46