OAI/Analysis/BiholderTransport/Regularity/JointMovingPrefix.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.joint_movingPrefix_contMDiffAt line 22
2. lemma OAI.WeakMTWTransport.joint_movingPrefixChart_contDiffAt line 29
3. lemma OAI.WeakMTWTransport.joint_movingPrefixEnergy_contDiffAt line 38
4. lemma OAI.WeakMTWTransport.movingPrefix_at_center line 61
5. lemma OAI.WeakMTWTransport.movingPrefixEnergy_hessian_at_center line 69