OAI/Analysis/LaughlinFock/CopyNormalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Copy Normalization.

  1. theorem OAI.LaughlinFock.antisymmetric_wedge_inner line 14
  2. def OAI.LaughlinFock.wedgeCoupledCoefficient line 54
  3. theorem OAI.LaughlinFock.gridInner_eq_fin_sum line 57
  4. theorem OAI.LaughlinFock.wedgeCoupledCoefficient_gram line 70
  5. theorem OAI.LaughlinFock.tensor_contraction_inner line 86
  6. def OAI.LaughlinFock.composedCoupledVector line 113
  7. theorem OAI.LaughlinFock.composedCoupledVector_gram line 121
  8. theorem OAI.LaughlinFock.composedCoupledVector_eq_sphericalCopy line 152
  9. theorem OAI.LaughlinFock.sphericalCopyCoefficient_highest_gram line 198