OAI/Geometry/NodalSets/Charts/RoundCotangentTensor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Target.sphereRoundForm line 18
2. lemma OAI.Yau.Target.sphereRoundForm_pos line 21
3. def OAI.Yau.Target.sphereRoundMusical line 28
4. def OAI.Yau.Target.sphereCotangentRepresentative line 31
5. lemma OAI.Yau.Target.sphereCotangentRepresentative_pair line 34
6. lemma OAI.Yau.Target.sphereCotangentRepresentative_restriction line 39
7. lemma OAI.Yau.Target.sphereCotangentRepresentative_orthogonal line 44
8. lemma OAI.Yau.Target.sphereCotangentRepresentative_unique line 49
9. lemma OAI.Yau.Target.sphereCotangentRepresentative_project line 57
10. def OAI.Yau.Target.roundCotangentTensor line 62
11. lemma OAI.Yau.Target.roundCotangentTensor_apply line 65
12. lemma OAI.Yau.Target.roundCotangentTensor_symm line 69
13. lemma OAI.Yau.Target.roundCotangentTensor_pos line 74
14. lemma OAI.Yau.Target.roundCotangentTensor_restriction line 83
15. lemma OAI.Yau.Target.roundCotangentTensor_tangent line 88
16. lemma OAI.Yau.Target.roundCotangentTensor_ambient line 93