OAI/Probability/InvariantIsing/Fields/VectorTerminalLabeled.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Original labeled Gibbs laws for finite Gaussian vector terminals.

  1. abbrev OAI.InvariantIsing.VectorTerminalCoordinates line 13
  2. def OAI.InvariantIsing.vectorTerminalCoordinateLaw line 15
  3. instance OAI.InvariantIsing.vectorTerminalCoordinateLaw_probability line 19
  4. def OAI.InvariantIsing.vectorLabeledTerminalLaw line 24
  5. instance OAI.InvariantIsing.vectorLabeledTerminalLaw_probability line 29
  6. lemma OAI.InvariantIsing.measurable_vectorLabeledTerminalLaw line 35
  7. lemma OAI.InvariantIsing.vectorLeafSum_labeled line 47