OAI/Probability/InvariantIsing/Cavity/CavityAffineFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

One spectrum on all sizes for each fixed vector of residue offsets.

  1. def OAI.InvariantIsing.cavityAffineLabel line 12
  2. lemma OAI.InvariantIsing.cavityAffineLabel_eq_ordered line 20
  3. lemma OAI.InvariantIsing.cavityAffineLabel_progression line 35
  4. lemma OAI.InvariantIsing.cavityAffineFullGroup_eq line 41
  5. lemma OAI.InvariantIsing.cavityAffineBase_label line 50
  6. lemma OAI.InvariantIsing.cavityAffineBase_canonical_label line 65
  7. lemma OAI.InvariantIsing.cavityAffineBase_partition line 74