OAI/Analysis/LaughlinFock/TensorIntegrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tensor Integrals.

  1. def OAI.LaughlinFock.copyBlock line 17
  2. def OAI.LaughlinFock.copyPartialTrace line 22
  3. def OAI.LaughlinFock.copyBlockLinear line 26
  4. theorem OAI.LaughlinFock.copyBlock_integral line 33
  5. theorem OAI.LaughlinFock.copyBlock_conjugation line 41
  6. theorem OAI.LaughlinFock.schur_multiplicity_average line 52
  7. theorem OAI.LaughlinFock.matrix_intertwiner_eq_zero_of_card_ne line 84
  8. theorem OAI.LaughlinFock.schur_cross_average line 107