OAI/Probability/InvariantIsing/Fields/FieldSpinPairConditioning.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Physical spins conditional on the two scalar-field endpoints.

  1. lemma OAI.InvariantIsing.field_two_gibbs_coordinate_mean line 14
  2. theorem OAI.InvariantIsing.field_leaf_spin_pair_conditioning line 30