OAI/Analysis/Brenier/Basic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem358.E line 12

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:12 (different declaration text). Qualify references as OAI.Problem358.E@path.

2. def OAI.Problem358.uniformMeasure line 14

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:14 (different declaration text). Qualify references as OAI.Problem358.uniformMeasure@path.

3. def OAI.Problem358.IsSupported line 17

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:17 (different declaration text). Qualify references as OAI.Problem358.IsSupported@path.

4. def OAI.Problem358.IsCoupling line 20

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:21 (different declaration text). Qualify references as OAI.Problem358.IsCoupling@path.

5. def OAI.Problem358.quadraticPlanCost line 26

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:27 (different declaration text). Qualify references as OAI.Problem358.quadraticPlanCost@path.

6. def OAI.Problem358.wasserstein2 line 29

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:31 (different declaration text). Qualify references as OAI.Problem358.wasserstein2@path.

7. def OAI.Problem358.graphPlan line 36

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:38 (different declaration text). Qualify references as OAI.Problem358.graphPlan@path.

8. def OAI.Problem358.IsQuadraticOptimalMap line 40

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:42 (different declaration text). Qualify references as OAI.Problem358.IsQuadraticOptimalMap@path.

9. def OAI.Problem358.IsUniqueQuadraticOptimalMap line 48

   Distinct definitions of this name: ComparatorChallenges/Brenier.lean:50 (different declaration text). Qualify references as OAI.Problem358.IsUniqueQuadraticOptimalMap@path.

10. def OAI.Problem358.mapL2Dist line 56

    Distinct definitions of this name: ComparatorChallenges/Brenier.lean:58 (different declaration text). Qualify references as OAI.Problem358.mapL2Dist@path.

11. def OAI.Problem358.cube line 60

    Distinct definitions of this name: ComparatorChallenges/Brenier.lean:62 (different declaration text). Qualify references as OAI.Problem358.cube@path.

12. def OAI.Problem358.HasExactlyThreeAtoms line 63

    Distinct definitions of this name: ComparatorChallenges/Brenier.lean:65 (different declaration text). Qualify references as OAI.Problem358.HasExactlyThreeAtoms@path.