OAI/Analysis/BiholderTransport/Regularity/MetricDefinitions.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakMTWTransport.cTransform line 16
  2. def OAI.WeakMTWTransport.IsCostDualPair line 19
  3. def OAI.WeakMTWTransport.contactGap line 22
  4. def OAI.WeakMTWTransport.gapSection line 25
  5. lemma OAI.WeakMTWTransport.continuous_cost_left line 28
  6. lemma OAI.WeakMTWTransport.continuous_cost_right line 31
  7. lemma OAI.WeakMTWTransport.cost_symm line 34
  8. lemma OAI.WeakMTWTransport.cost_nonneg line 37
  9. lemma OAI.WeakMTWTransport.cost_lipschitz_of_distance_bound line 40
  10. lemma OAI.WeakMTWTransport.exists_cTransform_contact line 56
  11. lemma OAI.WeakMTWTransport.cTransform_gap_nonneg line 70
  12. lemma OAI.WeakMTWTransport.cTransform_gap_zero line 76
  13. lemma OAI.WeakMTWTransport.cTransform_lipschitz line 84
  14. lemma OAI.WeakMTWTransport.continuous_cTransform line 101
  15. lemma OAI.WeakMTWTransport.dualPair_gap_nonneg line 108
  16. lemma OAI.WeakMTWTransport.dualPair_contact_left line 113
  17. lemma OAI.WeakMTWTransport.contactGap_symm line 119
  18. lemma OAI.WeakMTWTransport.dualPair_contact_right line 125
  19. lemma OAI.WeakMTWTransport.homeomorph_of_contact_bounds line 130
  20. lemma OAI.WeakMTWTransport.contactGap_le_of_contact line 175
  21. lemma OAI.WeakMTWTransport.contact_section_zero_diameter line 187
  22. lemma OAI.WeakMTWTransport.global_contact_bound_of_local line 208
  23. lemma OAI.WeakMTWTransport.contact_bound_of_section_bound line 235