OAI/Geometry/WeakHessian/Entropy/CostTopology.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakHessian.quadraticWassersteinSq_tendsto_zero_of_testsline 18 - lemma
OAI.WeakHessian.quadraticWassersteinSq_tendsto_pairline 42