OAI/Geometry/WeakHessian/LocalBounds/HopfInitialSlope.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.slopeApprox_quotient_le line 17
2. lemma OAI.WeakHessianTransport.hopf_initial_slopeApprox_bound line 30
3. lemma OAI.WeakHessianTransport.hopf_initial_quotient_nonneg line 45
4. lemma OAI.WeakHessianTransport.hopf_initial_quotient_le line 49
5. lemma OAI.WeakHessianTransport.tendsto_slopeApprox_toReal line 54
6. lemma OAI.WeakHessianTransport.hopf_initial_eventually_lt line 70