OAI/Analysis/BiholderTransport/Calculus/PathCalculus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.pathLinearApply line 44
2. lemma OAI.WeakMTWTransport.pathLinearApply_apply line 58
3. lemma OAI.WeakMTWTransport.norm_pathLinearApply_le line 61
4. def OAI.WeakMTWTransport.pathLinearApplyL line 70
5. lemma OAI.WeakMTWTransport.hasFDerivAt_path_comp line 81
6. lemma OAI.WeakMTWTransport.contDiff_path_comp_nat line 115
7. lemma OAI.WeakMTWTransport.contDiff_path_comp line 128