OAI/Analysis/CoulombTransport/GraphBridge.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem356.measurable_tripleFst line 11
  2. lemma OAI.Problem356.measurable_tripleSnd line 12
  3. lemma OAI.Problem356.measurable_tripleThd line 13
  4. lemma OAI.Problem356.measurable_invDistance line 15
  5. lemma OAI.Problem356.measurable_coulombCost line 19
  6. def OAI.Problem356.graphMap line 25
  7. def OAI.Problem356.graphMeasure line 27
  8. lemma OAI.Problem356.measurable_graphMap line 30
  9. lemma OAI.Problem356.graphMeasure_isThreeCoupling line 33
  10. lemma OAI.Problem356.lintegral_graphMeasure line 47
  11. lemma OAI.Problem356.kantorovichValue_le_graphCost line 52
  12. lemma OAI.Problem356.kantorovichValue_le_mongeValue line 58