OAI/Analysis/BiholderTransport/LinearAlgebra/BilinearMatrix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.bilinearMatrix line 17
2. lemma OAI.WeakMTWTransport.bilinearMatrix_det line 22
3. lemma OAI.WeakMTWTransport.bilinearMatrix_quad line 26
4. lemma OAI.WeakMTWTransport.bilinearMatrix_nonneg line 45
5. lemma OAI.WeakMTWTransport.bilinear_positive_of_det_ne_zero line 55
6. lemma OAI.WeakMTWTransport.bilinear_det_nonneg line 69
7. lemma OAI.WeakMTWTransport.bilinearOperator_tendsto line 75
8. lemma OAI.WeakMTWTransport.bilinear_det_tendsto line 83