OAI/Analysis/Laughlin/Fock/ContractionBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.sum_unoccupied_insert line 8
  2. theorem OAI.Laughlin.Fock.annihilate_normSq line 27
  3. theorem OAI.Laughlin.Fock.annihilate_normSq_le line 39
  4. theorem OAI.Laughlin.Fock.two_annihilate_normSq_le line 49
  5. theorem OAI.Laughlin.Fock.sourceFour_normSq_le_pair line 53
  6. theorem OAI.Laughlin.Fock.limitFour_normSq_le_pair line 58