OAI/Probability/InvariantIsing/Magnetic/RestrictedRotationProbability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual constrained spin/leaf Gibbs probability, with all Haar, Gaussian and finite-tree disorder retained.

  1. def OAI.InvariantIsing.restrictedRotationProbability line 14
  2. instance OAI.InvariantIsing.restrictedRotationProbability_probability line 22
  3. lemma OAI.InvariantIsing.measurable_restrictedRotationProbability line 29
  4. lemma OAI.InvariantIsing.restricted_rotation_exp_integrable_ae line 49
  5. lemma OAI.InvariantIsing.restrictedRotationProbability_eq_tilted_ae line 64