OAI/Probability/InvariantIsing/Fields/FieldWasserstein.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

First-moment transport is the infimum of the costs of joint laws.

  1. structure OAI.InvariantIsing.FieldLawCoupling line 12

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:197 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.FieldLawCoupling@path.

  2. def OAI.InvariantIsing.FieldLawCoupling.cost line 21

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:202 (different declaration text). Qualify references as OAI.InvariantIsing.FieldLawCoupling.cost@path.

  3. lemma OAI.InvariantIsing.FieldLawCoupling.integrable_fst line 24
  4. lemma OAI.InvariantIsing.FieldLawCoupling.integrable_snd line 30
  5. lemma OAI.InvariantIsing.FieldLawCoupling.cost_eq_ofReal line 36
  6. def OAI.InvariantIsing.fieldWassersteinOne line 46

    Also declared: ComparatorChallenges/InvariantIsing.lean:205 (same declaration text).

  7. lemma OAI.InvariantIsing.exists_fieldLawCoupling_cost_lt line 49