OAI/Analysis/BiholderTransport/Regularity/MovingPrefix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.movingPrefix line 20
2. def OAI.WeakMTWTransport.movingPrefixChart line 21
3. def OAI.WeakMTWTransport.movingPrefixEnergy line 23
4. lemma OAI.WeakMTWTransport.movingPrefix_contMDiffAt line 26
5. lemma OAI.WeakMTWTransport.movingPrefixChart_contDiffAt line 33
6. lemma OAI.WeakMTWTransport.movingPrefix_eq line 44
7. lemma OAI.WeakMTWTransport.movingPrefixEnergy_contDiffAt line 51
8. lemma OAI.WeakMTWTransport.movingPrefixEnergy_axis_near line 70
9. lemma OAI.WeakMTWTransport.movingPrefixEnergy_hessian line 84