OAI/Probability/InvariantIsing/Magnetic/RestrictedPairSpinKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two constrained spins sampled independently after a prescribed common Gaussian prefix. The common prefix is retained in the actual kernel law.

  1. def OAI.InvariantIsing.restrictedPairSpinKernel line 15
  2. instance OAI.InvariantIsing.restrictedPairSpinKernel_markov line 29