OAI/Probability/InvariantIsing/Fields/RationalFieldLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite positive rational field laws used in the W1 extension of the magnetic pressure formula. Labels may repeat the same field value.

  1. structure OAI.InvariantIsing.RationalFieldLaw line 12
  2. def OAI.InvariantIsing.RationalFieldLaw.mass line 21
  3. lemma OAI.InvariantIsing.RationalFieldLaw.mass_pos line 23
  4. lemma OAI.InvariantIsing.RationalFieldLaw.mass_sum line 27
  5. def OAI.InvariantIsing.RationalFieldLaw.measure line 31
  6. instance OAI.InvariantIsing.RationalFieldLaw.probability line 33
  7. def OAI.InvariantIsing.RationalFieldLaw.law line 36
  8. def OAI.InvariantIsing.RationalFieldLaw.magneticValue line 38
  9. lemma OAI.InvariantIsing.RationalFieldLaw.magneticValue_eq_of_law_eq line 41
  10. lemma OAI.InvariantIsing.RationalFieldLaw.integrable_id line 51