OAI/Analysis/Mahler/ReferencePoleFrame.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Mahler.poleFrameVector line 10
2. lemma OAI.Mahler.poleFrameVector_tangent line 15
3. def OAI.Mahler.poleTangentFrame line 20
4. lemma OAI.Mahler.pole_covector_matrix line 24
5. lemma OAI.Mahler.referencePole_boundary_value line 55
6. lemma OAI.Mahler.ambientFinEquiv_real_zero line 65
7. lemma OAI.Mahler.ambientFinEquiv_imag_zero line 70
8. lemma OAI.Mahler.ambientFinEquiv_tail line 75
9. def OAI.Mahler.poleFrameFin line 81
10. lemma OAI.Mahler.poleFrameFin_volume line 84
11. lemma OAI.Mahler.referencePole_boundaryFin_value line 107