OAI/MathematicalPhysics/BFSS/OscillatorForms.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Normal core energy identities, positivity and compact multipliers.

  1. def OAI.BFSSQuantum.AlgebraData.normalChargeField line 17
  2. lemma OAI.BFSSQuantum.AlgebraData.normalChargeField_apply line 22
  3. lemma OAI.BFSSQuantum.AlgebraData.normalChargeField_basis line 25
  4. abbrev OAI.BFSSQuantum.AlgebraData.NormalCore line 31
  5. def OAI.BFSSQuantum.AlgebraData.normalCoreCharge line 33
  6. lemma OAI.BFSSQuantum.AlgebraData.normalSkewCore_apply line 37
  7. lemma OAI.BFSSQuantum.AlgebraData.normalSkewCore_norm line 47
  8. lemma OAI.BFSSQuantum.AlgebraData.normalRemainderField_apply line 67
  9. theorem OAI.BFSSQuantum.AlgebraData.normalCore_energy_identity line 75
  10. theorem OAI.BFSSQuantum.AlgebraData.normalOscillator_core_nonneg line 125
  11. def OAI.BFSSLocalL2.compactBound line 153
  12. lemma OAI.BFSSLocalL2.compactBound_nonneg line 157
  13. lemma OAI.BFSSLocalL2.compactBound_bound line 161
  14. def OAI.BFSSLocalL2.compactMul line 165
  15. lemma OAI.BFSSLocalL2.compactMul_ae line 170
  16. lemma OAI.BFSSLocalL2.compactMul_continuous line 174