OAI/Analysis/BiholderTransport/LinearAlgebra/SpectralContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.ordered_eigenvalues_positive_crossing line 17
2. def OAI.WeakMTWTransport.middleHessianOperator line 55
3. lemma OAI.WeakMTWTransport.inner_middleHessianOperator line 62
4. lemma OAI.WeakMTWTransport.middleHessianOperator_symmetric line 67
5. lemma OAI.WeakMTWTransport.shortened_middle_operator_positive line 78
6. lemma OAI.WeakMTWTransport.uniform_middle_ordered_crossing line 93