OAI/Probability/InvariantIsing/Cavity/CavityPrefixAffineFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

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

  1. def OAI.InvariantIsing.cavityPrefixAffineSize line 13
  2. lemma OAI.InvariantIsing.cavityPrefixAffineCount_sum line 16
  3. lemma OAI.InvariantIsing.cavityPrefixAffineFull_sum line 21
  4. def OAI.InvariantIsing.cavityPrefixAffineFullGroup line 27
  5. def OAI.InvariantIsing.cavityPrefixAffineRetainedEquiv line 32
  6. def OAI.InvariantIsing.cavityPrefixAffineBaseEquiv line 40
  7. lemma OAI.InvariantIsing.cavityPrefixAffineLabel_progression line 49
  8. lemma OAI.InvariantIsing.cavityPrefixAffineFullGroup_eq line 55
  9. lemma OAI.InvariantIsing.cavityPrefixAffineBase_label line 64
  10. lemma OAI.InvariantIsing.cavityPrefixAffineBase_canonical_label line 79
  11. lemma OAI.InvariantIsing.cavityPrefixAffineBase_partition line 88