OAI/Analysis/AffineBernstein/TubeFrame.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.support_angular_derivative line 18
2. def OAI.AffineBernstein.tubeBaseMatrix line 32
3. def OAI.AffineBernstein.tubeRadiusMatrix line 36
4. def OAI.AffineBernstein.tubeTangent line 40
5. def OAI.AffineBernstein.tubeFrame line 43
6. lemma OAI.AffineBernstein.tubeSecondForm_blocks line 50
7. lemma OAI.AffineBernstein.tubeFrame_matrix line 65
8. lemma OAI.AffineBernstein.tubeFrame_det line 98