OAI/Analysis/BiholderTransport/Regularity/CompactAE.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.contact_gap_control_at line 20
2. lemma OAI.WeakMTWTransport.transform_perturbation_upper_at line 50
3. def OAI.WeakMTWTransport.transformedDifferenceQuotient line 80
4. lemma OAI.WeakMTWTransport.transformedDifferenceQuotient_apply line 83
5. lemma OAI.WeakMTWTransport.transformedDifferenceQuotient_norm_le line 91
6. lemma OAI.WeakMTWTransport.transformedDifferenceQuotient_tendsto_at line 103
7. lemma OAI.WeakMTWTransport.dual_minimum_ae_integral_eq line 134
8. lemma OAI.WeakMTWTransport.cost_contact_relation_isClosed line 184
9. lemma OAI.WeakMTWTransport.dual_minimum_ae_pushforward line 191