OAI/Probability/InvariantIsing/Fields/SpinPriorFieldMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact zero-temperature constrained field value, including the finite constraint's probability normalization.

  1. lemma OAI.InvariantIsing.spinPriorMeanPressure_field line 16
  2. lemma OAI.InvariantIsing.spinPriorMeanPressure_restricted_field line 75