OAI/Probability/InvariantIsing/Cavity/CavityRetainedStack.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Assemble the retained group frames without imposing equal group sizes. The separate group projector identities give completeness.

  1. def OAI.InvariantIsing.cavityRetainedStack line 13
  2. theorem OAI.InvariantIsing.cavityRetainedStack_gram line 17
  3. theorem OAI.InvariantIsing.cavityRetainedStack_outer line 33
  4. theorem OAI.InvariantIsing.cavityEigenspaceFrame_outer line 41
  5. theorem OAI.InvariantIsing.cavityRetainedStack_complete line 53