OAI/Analysis/BiholderTransport/LinearAlgebra/MiddleScaling.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.middleHessian_scaled_ray line 25
2. lemma OAI.WeakMTWTransport.ordered_singularValues_positive_smul line 65
3. def OAI.WeakMTWTransport.intrinsicBilinearOperator line 106
4. def OAI.WeakMTWTransport.intrinsicBilinearSingular line 111
5. lemma OAI.WeakMTWTransport.intrinsicBilinearSingular_heq line 119
6. lemma OAI.WeakMTWTransport.intrinsicBilinearOperator_smul line 132
7. lemma OAI.WeakMTWTransport.intrinsicBilinearSingular_pos_smul line 142
8. def OAI.WeakMTWTransport.middleSingularValue line 150
9. lemma OAI.WeakMTWTransport.middleSingularValue_scaled_ray line 154