OAI/Probability/InvariantIsing/Magnetic/RestrictedPriorPressure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact pressure transport from the constrained physical rotation to its fixed-prior realization. Normalization is kept separate from the cube mass.

  1. lemma OAI.InvariantIsing.restricted_special_prior_log_mean line 15
  2. lemma OAI.InvariantIsing.restricted_prior_pressure_mean line 29