OAI/Analysis/BiholderTransport/Calculus/CompactParameterJets.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.compact_parameter_second_jet line 18
2. def OAI.WeakMTWTransport.shortLegCost line 58
3. def OAI.WeakMTWTransport.movingShortLegCost line 61
4. lemma OAI.WeakMTWTransport.movingShortLegCost_contDiffAt line 64
5. lemma OAI.WeakMTWTransport.shortLeg_second_bound_near_base line 88
6. lemma OAI.WeakMTWTransport.exists_uniform_shortLeg_second_bound line 140