OAI/Geometry/WeakHessian/Transport/AeProdMetricSpeed.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsTestPlan.ae_prod_metricSpeed_lt_top line 20
2. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.of_dominated_ae_tendsto line 30