OAI/Analysis/BiholderTransport/CostGeometry/CurveAdvance.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.curve_deriv_eq_active_pairing line 18
2. lemma OAI.WeakMTWTransport.curve_neg_cost_deriv_eq_pairing line 50
3. lemma OAI.WeakMTWTransport.spray_neg_cost_deriv_le line 84
4. lemma OAI.WeakMTWTransport.curve_deriv_le_active_norm line 101
5. lemma OAI.WeakMTWTransport.spray_deriv_le_active_norm line 110