OAI/Analysis/BiholderTransport/Regularity/SplitEndpointCost.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.splitEndpointCost line 19
2. lemma OAI.WeakMTWTransport.splitEndpointCost_contDiffAt line 23
3. lemma OAI.WeakMTWTransport.splitEndpointCost_axis line 33
4. lemma OAI.WeakMTWTransport.splitEndpointCost_axis_near line 52
5. lemma OAI.WeakMTWTransport.splitEndpointCost_source_gradient line 61
6. lemma OAI.WeakMTWTransport.splitEndpointCost_mixed line 82