OAI/Analysis/BiholderTransport/CostGeometry/SplitTrial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.splitTrialValue line 139
2. lemma OAI.WeakMTWTransport.splitTrialValue_contDiffAt line 142
3. lemma OAI.WeakMTWTransport.splitTrialValue_eq_hessian line 157
4. lemma OAI.WeakMTWTransport.splitTrialValue_middle_eq_diagonal line 170
5. lemma OAI.WeakMTWTransport.splitTrialValue_nonneg line 181
6. lemma OAI.WeakMTWTransport.splitTrialValue_conjugate_null line 203
7. lemma OAI.WeakMTWTransport.splitTrialValue_schur line 212