OAI/Analysis/LaughlinFock/ScalarAction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Scalar Action.

  1. theorem OAI.LaughlinFock.gridInner_self_eq_zero line 13
  2. theorem OAI.LaughlinFock.coupledVector_lowest line 30
  3. theorem OAI.LaughlinFock.coupledVector_outside_ladder line 52
  4. theorem OAI.LaughlinFock.coupledVector_lower_all line 60
  5. theorem OAI.LaughlinFock.coupledVector_raise_all line 70
  6. theorem OAI.LaughlinFock.grid_highest_eq_of_first line 80
  7. theorem OAI.LaughlinFock.highestCoefficient_first_ne_zero line 105
  8. theorem OAI.LaughlinFock.grid_highest_unique line 117
  9. theorem OAI.LaughlinFock.coupledVector_intertwiner line 131