OAI/Geometry/WeakHessian/Transport/DerivEventuallyUpperRight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.deriv_le_of_eventually_upper_right_slope line 45
2. lemma OAI.WeakHessianTransport.sub_le_integral_of_upper_right_slope line 55