OAI/Probability/InvariantIsing/Fields/MarkEndpointKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Endpoint kernels of the finite ancestor-dependent increment chain.

  1. def OAI.InvariantIsing.markStateKernel line 13
  2. instance OAI.InvariantIsing.markStateKernel_markov line 17
  3. lemma OAI.InvariantIsing.markStateKernel_apply line 22
  4. def OAI.InvariantIsing.markTailEndpointKernel line 31
  5. instance OAI.InvariantIsing.markTailEndpointKernel_markov line 36
  6. def OAI.InvariantIsing.markPairEndpointKernel line 46
  7. instance OAI.InvariantIsing.markPairEndpointKernel_markov line 52