OAI/Probability/InvariantIsing/Cavity/CavityBaseGroups.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Grouping retained and exceptional base axes by the same spectral labels. Their dimensions are the retained counts plus the finite extras.

  1. def OAI.InvariantIsing.cavityBaseGroupSumEquiv line 13
  2. lemma OAI.InvariantIsing.cavityBaseGroupSumEquiv_label line 30
  3. def OAI.InvariantIsing.cavityBaseGroupDimension line 37
  4. def OAI.InvariantIsing.cavityBaseGroupEquiv line 40
  5. lemma OAI.InvariantIsing.cavityBaseGroupEquiv_label line 47
  6. lemma OAI.InvariantIsing.cavityBaseGroupDimension_ge line 59
  7. theorem OAI.InvariantIsing.cavity_canonical_group_frames line 62