OAI/Probability/InvariantIsing/Fields/FieldVectorSampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual vector spin sampling for independent scalar cavity fields.

  1. lemma OAI.InvariantIsing.measurable_field_product line 14
  2. def OAI.InvariantIsing.fieldVectorTransitionKernel line 39
  3. instance OAI.InvariantIsing.fieldVectorTransitionKernel_markov line 44
  4. lemma OAI.InvariantIsing.fieldVectorTransitionKernel_eq_tilted line 49
  5. lemma OAI.InvariantIsing.fieldVectorTransitionKernel_coordinate line 55
  6. def OAI.InvariantIsing.fieldVectorSpinKernel line 64
  7. instance OAI.InvariantIsing.fieldVectorSpinKernel_markov line 71
  8. def OAI.InvariantIsing.fieldVectorTailSpinKernel line 78
  9. instance OAI.InvariantIsing.fieldVectorTailSpinKernel_markov line 88
  10. theorem OAI.InvariantIsing.fieldVectorTailSpinKernel_coordinate_mean line 98