OAI/Analysis/BiholderTransport/Duality/CompactDual.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.cTransform_le_iff line 17
  2. lemma OAI.WeakMTWTransport.cTransform_antitone line 27
  3. lemma OAI.WeakMTWTransport.cTransform_cTransform_le line 35
  4. lemma OAI.WeakMTWTransport.cTransform_triple line 43
  5. lemma OAI.WeakMTWTransport.cTransform_add_const line 50
  6. lemma OAI.WeakMTWTransport.cTransform_zero line 63
  7. def OAI.WeakMTWTransport.boundedCTransform line 72
  8. lemma OAI.WeakMTWTransport.boundedCTransform_apply line 75
  9. lemma OAI.WeakMTWTransport.boundedCTransform_nonexpansive line 78
  10. lemma OAI.WeakMTWTransport.isCompact_bounded_lipschitz line 102
  11. def OAI.WeakMTWTransport.normalizedDualPairs line 131
  12. lemma OAI.WeakMTWTransport.isClosed_normalizedDualPairs line 134
  13. lemma OAI.WeakMTWTransport.normalizedDualPairs_nonempty line 142
  14. lemma OAI.WeakMTWTransport.normalizedDualPairs_bounds line 148
  15. lemma OAI.WeakMTWTransport.isCompact_normalizedDualPairs line 178
  16. lemma OAI.WeakMTWTransport.integral_boundedContinuous_lipschitz line 191
  17. def OAI.WeakMTWTransport.dualObjective line 201
  18. lemma OAI.WeakMTWTransport.continuous_dualObjective line 205
  19. lemma OAI.WeakMTWTransport.exists_minimizing_normalizedDualPair line 210
  20. def OAI.WeakMTWTransport.normalizeDualPair line 216
  21. lemma OAI.WeakMTWTransport.normalizeDualPair_mem line 222
  22. lemma OAI.WeakMTWTransport.dualObjective_add_constants line 241
  23. lemma OAI.WeakMTWTransport.dualObjective_normalize_le line 252