OAI/Analysis/BiholderTransport/LinearAlgebra/BilinearDet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.bilinearMatrix_apply line 18
2. lemma OAI.WeakMTWTransport.functional_coords_dot line 25
3. lemma OAI.WeakMTWTransport.bilinearMatrix_symmetric line 31
4. lemma OAI.WeakMTWTransport.bilinearMatrix_positive line 36
5. lemma OAI.WeakMTWTransport.bilinearMatrix_le line 47
6. lemma OAI.WeakMTWTransport.bilinearMatrix_rank_add line 57
7. lemma OAI.WeakMTWTransport.bilinear_determinant_gain line 65