OAI/Analysis/BiholderTransport/Regularity/UniformMixedBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.movingNormalEndpointJoinAction_chart_contDiffAt line 20
2. def OAI.WeakMTWTransport.movingEndpointFamily line 41
3. lemma OAI.WeakMTWTransport.movingEndpointFamily_contDiffAt line 49
4. lemma OAI.WeakMTWTransport.compact_movingEndpointFamily_bound line 58
5. lemma OAI.WeakMTWTransport.normalEndpointMixedOperator_bound_near_pair line 83
6. lemma OAI.WeakMTWTransport.normalEndpointMixedOperator_uniform_bound line 118