OAI/Probability/InvariantIsing/Cavity/CavityBasePerturbedLaw.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The physical base array uses the very same finite perturbation minimizers as the tensor GG construction.

  1. lemma OAI.InvariantIsing.cavity_base_perturbed_array_law line 15
  2. theorem OAI.InvariantIsing.cavity_rotation_minimizers_spectralGG line 26