OAI/Probability/InvariantIsing/Fields/FieldVectorPairSampling.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Evaluation of the common-prefix vector Ising spin pair law, with the actual cascade depth distribution and its independent root Gaussian.

  1. def OAI.InvariantIsing.fieldVectorPairSpinKernel line 16
  2. instance OAI.InvariantIsing.fieldVectorPairSpinKernel_markov line 28
  3. theorem OAI.InvariantIsing.fieldVectorPairSpinKernel_coordinate_mean line 43
  4. def OAI.InvariantIsing.fieldVectorLevelSpinPair line 81
  5. instance OAI.InvariantIsing.fieldVectorLevelSpinPair_probability line 87
  6. theorem OAI.InvariantIsing.fieldVectorLevelSpinPair_coordinate_mean line 92
  7. theorem OAI.InvariantIsing.fieldVectorLevelSpinPair_cascade_test line 111
  8. theorem OAI.InvariantIsing.fieldVectorLevelSpinPair_centered_test line 121