OAI/Probability/InvariantIsing/Cavity/CavityOrientationProbability.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Orienting the eigenbasis preserves the whole random Gibbs probability, and identifies it with the published-input tensor realization.

  1. lemma OAI.InvariantIsing.cavityOrientationLift_perturbation_covariance line 15
  2. theorem OAI.InvariantIsing.cavity_orientation_probability_law line 25
  3. theorem OAI.InvariantIsing.cavity_orientation_tensor_probability_law line 43