OAI/Analysis/BiholderTransport/Regularity/UnitTime.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakMTWTransport.UnitTime line 35
2. def OAI.WeakMTWTransport.extendUnitPath line 40
3. lemma OAI.WeakMTWTransport.extendUnitPath_coe line 44
4. lemma OAI.WeakMTWTransport.extendUnitPath_add line 50
5. lemma OAI.WeakMTWTransport.extendUnitPath_smul line 53
6. def OAI.WeakMTWTransport.unitPathPrimitive line 56
7. lemma OAI.WeakMTWTransport.unitPathPrimitive_bound line 62
8. def OAI.WeakMTWTransport.unitPathIntegral line 73
9. lemma OAI.WeakMTWTransport.unitPathIntegral_apply line 96
10. lemma OAI.WeakMTWTransport.hasDerivAt_unitPathPrimitive line 99