OAI/Analysis/BiholderTransport/Regularity/NormMinMax.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.paired_basis_slice_map line 21
2. lemma OAI.WeakMTWTransport.quadratic_lower_spectral_slice line 61
3. lemma OAI.WeakMTWTransport.quadratic_upper_spectral_slice line 73
4. lemma OAI.WeakMTWTransport.ordered_eigenvalue_pullback_comparison line 85
5. lemma OAI.WeakMTWTransport.ordered_singularValues_pullback line 104