OAI/Probability/InvariantIsing/Core/FiniteFieldTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite transport plans for rational field laws and the magnetic one-Lipschitz estimate against every such plan.

  1. structure OAI.InvariantIsing.RationalFieldLaw.Coupling line 12
  2. def OAI.InvariantIsing.RationalFieldLaw.Coupling.independent line 22
  3. instance OAI.InvariantIsing.RationalFieldLaw.Coupling.(instance at line 28) line 28
  4. def OAI.InvariantIsing.RationalFieldLaw.Coupling.cost line 30
  5. lemma OAI.InvariantIsing.RationalFieldLaw.Coupling.cost_nonneg line 32
  6. def OAI.InvariantIsing.RationalFieldLaw.Coupling.flip line 36
  7. lemma OAI.InvariantIsing.RationalFieldLaw.Coupling.flip_cost line 42
  8. lemma OAI.InvariantIsing.RationalFieldLaw.Coupling.magneticValue_sub_le_cost line 47
  9. lemma OAI.InvariantIsing.RationalFieldLaw.Coupling.abs_magneticValue_sub_le_cost line 59