OAI/Analysis/Laughlin/FourBody/TargetBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Laughlin.Fock.castSpinColumns_mul_adjoint line 10
  2. theorem OAI.Laughlin.Fock.fourWedgeProjector_congr line 16
  3. theorem OAI.Laughlin.Fock.retainedFirst_projector line 24
  4. theorem OAI.Laughlin.Fock.contractionForm_projector_nonneg line 33
  5. theorem OAI.Laughlin.Fock.sum_fin_castLE_le line 38
  6. theorem OAI.Laughlin.Fock.retainedFourTarget_le_full line 49