OAI/Geometry/SmoothYau/Estimates/QuadraticInnerSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.QuadraticInnerSpace line 20
2. instance OAI.YauCounterexamples.QuadraticInnerSpace.(instance at line 24) line 24
3. instance OAI.YauCounterexamples.QuadraticInnerSpace.(instance at line 25) line 25
4. instance OAI.YauCounterexamples.QuadraticInnerSpace.(instance at line 26) line 26
5. lemma OAI.YauCounterexamples.QuadraticInnerSpace.norm_sq line 29
6. def OAI.YauCounterexamples.quadraticNormEquiv line 39
7. lemma OAI.YauCounterexamples.quadraticNormEquiv_apply line 45
8. lemma OAI.YauCounterexamples.quadraticNormEquiv_norm_sq line 53