OAI/Analysis/BiholderTransport/LinearAlgebra/MixedOperator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.mixedOperator line 13
2. lemma OAI.WeakMTWTransport.mixedOperator_inner line 17
3. lemma OAI.WeakMTWTransport.mixedOperator_norm_le line 22
4. lemma OAI.WeakMTWTransport.mixed_factor_adjoint line 34
5. lemma OAI.WeakMTWTransport.factor_surjective_of_right_inverse line 52