OAI/Analysis/CoulombTransport/Model.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem356.E3 line 12

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:12 (same declaration text).

2. abbrev OAI.Problem356.Triple line 14

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:14 (same declaration text).

3. def OAI.Problem356.tripleFst line 16

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:16 (same declaration text).

4. def OAI.Problem356.tripleSnd line 18

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:18 (same declaration text).

5. def OAI.Problem356.tripleThd line 20

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:20 (same declaration text).

6. def OAI.Problem356.invDistance line 22

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:22 (same declaration text).

7. def OAI.Problem356.coulombCost line 25

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:25 (same declaration text).

8. def OAI.Problem356.IsThreeCoupling line 30

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:30 (same declaration text).

9. def OAI.Problem356.densityMeasure line 36

   Also declared: ComparatorChallenges/CoulombCounterexample.lean:36 (same declaration text).

10. def OAI.Problem356.Preserves line 39

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:39 (same declaration text).

11. def OAI.Problem356.graphCost line 42

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:42 (same declaration text).

12. def OAI.Problem356.kantorovichValue line 45

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:45 (same declaration text).

13. def OAI.Problem356.mongeValue line 49

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:49 (same declaration text).

14. def OAI.Problem356.IsSmoothCompactProbabilityDensity line 54

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:54 (same declaration text).

15. def OAI.Problem356.KantorovichAttained line 62

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:62 (same declaration text).

16. def OAI.Problem356.NoMongeOptimizer line 67

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:67 (same declaration text).

17. def OAI.Problem356.FiniteMongeApproximation line 72

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:72 (same declaration text).

18. def OAI.Problem356.HasCoulombCounterexample line 81

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:81 (same declaration text).

19. def OAI.Problem356.HasFullCoulombConclusion line 88

    Also declared: ComparatorChallenges/CoulombCounterexample.lean:88 (same declaration text).