OAI/Probability/InvariantIsing/Fields/FieldEndpointSampling.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Conditional Gaussian endpoint kernels before sampling the cavity spins.

  1. lemma OAI.InvariantIsing.field_tanh_measurable line 13
  2. def OAI.InvariantIsing.fieldVectorTailEndpointKernel line 18
  3. instance OAI.InvariantIsing.fieldVectorTailEndpointKernel_markov line 28
  4. lemma OAI.InvariantIsing.field_tanh_integrable line 39
  5. theorem OAI.InvariantIsing.fieldVectorTailEndpointKernel_coordinate_mean line 46
  6. def OAI.InvariantIsing.fieldVectorPairEndpointKernel line 66
  7. instance OAI.InvariantIsing.fieldVectorPairEndpointKernel_markov line 79
  8. lemma OAI.InvariantIsing.field_tanh_pair_integrable line 94
  9. theorem OAI.InvariantIsing.fieldVectorPairEndpointKernel_coordinate_mean line 105