OAI/Analysis/BiholderTransport/LocalFlow/CotangentFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakMTWTransport.Phase line 19
2. def OAI.WeakMTWTransport.phaseRaise line 21
3. def OAI.WeakMTWTransport.phaseLower line 24
4. def OAI.WeakMTWTransport.coordinatePhaseFlow line 27
5. lemma OAI.WeakMTWTransport.phaseLower_contDiffAt line 33
6. lemma OAI.WeakMTWTransport.phaseLower_raise line 44
7. lemma OAI.WeakMTWTransport.coordinatePhaseFlow_zero line 49
8. lemma OAI.WeakMTWTransport.coordinatePhaseFlow_contDiffAt line 59
9. lemma OAI.WeakMTWTransport.coordinatePhaseFlow_derivative_limit line 87