OAI/Analysis/LaughlinFock/HighestTails.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Highest Tails.

  1. theorem OAI.LaughlinFock.sum_gram_comparison line 14
  2. theorem OAI.LaughlinFock.highestFourAnnihilator_pair_posSemidef line 36
  3. theorem OAI.LaughlinFock.unit_vector_contracts_family line 44
  4. def OAI.LaughlinFock.highestThreeAnnihilator line 63
  5. theorem OAI.LaughlinFock.highestThreeAnnihilator_bound line 69
  6. theorem OAI.LaughlinFock.highestThreeAnnihilator_pair_posSemidef line 91
  7. theorem OAI.LaughlinFock.wedgeAnnihilator_mulVec line 104
  8. theorem OAI.LaughlinFock.threeWedgeMatrix_annihilator_column line 115
  9. theorem OAI.LaughlinFock.highestThreeAnnihilator_eq_wedge line 123
  10. theorem OAI.LaughlinFock.threeSpinProjection_trace line 155