OAI/Analysis/BiholderTransport/LinearAlgebra/CongruenceSpectrum.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.ordered_eigenvalues_bounded_congruence line 16
2. lemma OAI.WeakMTWTransport.middleHessianOperator_positive_one line 70
3. lemma OAI.WeakMTWTransport.uniform_join_middle_ordered_comparison line 79
4. lemma OAI.WeakMTWTransport.uniform_endpoint_middle_ordered_comparison line 105