OAI/Probability/InvariantIsing/Fields/VectorTerminalNoise.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Terminal Gibbs sampling and retained trees for finite vector fields.

  1. def OAI.InvariantIsing.vectorLeafSum line 14
  2. lemma OAI.InvariantIsing.measurable_vectorLeafSum line 18
  3. lemma OAI.InvariantIsing.noiseLeafTerminal_vector_sum line 24
  4. def OAI.InvariantIsing.vectorTerminalNoiseLaw line 36
  5. instance OAI.InvariantIsing.vectorTerminalNoiseLaw_probability line 41
  6. lemma OAI.InvariantIsing.measurable_vectorTerminalNoiseLaw line 45
  7. lemma OAI.InvariantIsing.vectorTerminalNoiseLaw_eq_backward line 51
  8. lemma OAI.InvariantIsing.vectorTerminalNoiseLaw_keep_ae line 66