OAI/Analysis/BiholderTransport/Contact/ActiveContinuationLocal.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.smooth_lower_support_mem_normalSubdifferentialline 220 - lemma
OAI.WeakMTWTransport.local_min_divided_cost_subgradientline 229 - lemma
OAI.WeakMTWTransport.WeakMTW.active_hull_nearby_local_minline 253