OAI/Analysis/BiholderTransport/LinearAlgebra/SplitEndpointJets.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.WeakMTWTransport.splitEndpointCost_source_hessianline 19 - lemma
OAI.WeakMTWTransport.splitEndpointCost_endpoint_gradientline 40 - lemma
OAI.WeakMTWTransport.splitEndpointCost_endpoint_hessianline 58 - lemma
OAI.WeakMTWTransport.splitEndpointCost_hessian_diagline 78