OAI/Probability/InvariantIsing/Cavity/CavitySelectedGroupFrames.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Completion of the selected canonical axes to a fixed orthonormal frame in each spectral group. Only finitely many cavity axes are added.

  1. def OAI.InvariantIsing.cavityGroupIndexEquiv line 14
  2. lemma OAI.InvariantIsing.cavityGroupIndexEquiv_apply line 20
  3. lemma OAI.InvariantIsing.cavity_group_selected_embedding line 24
  4. def OAI.InvariantIsing.cavitySelectedGroupFrame line 50
  5. lemma OAI.InvariantIsing.cavitySelectedGroupFrame_gram line 54
  6. lemma OAI.InvariantIsing.cavitySelectedGroupFrame_columns line 62