OAI/MathematicalPhysics/BFSS/NormalGap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Positive normal-form gap and nonzero zero-form extraction.

  1. def OAI.BFSSQuantum.AlgebraData.NormalZeroOrthogonal line 16
  2. theorem OAI.BFSSQuantum.AlgebraData.normal_unit_gap line 22
  3. lemma OAI.BFSSNormalAnalysis.moment_smul_memLp line 68
  4. lemma OAI.BFSSNormalAnalysis.moment_smul_toLp line 77
  5. lemma OAI.BFSSNormalAnalysis.weighted_energy_smul line 87
  6. lemma OAI.BFSSQuantum.AlgebraData.NormalFormDomain.smul line 111
  7. lemma OAI.BFSSQuantum.AlgebraData.normalOscillator_smul line 118
  8. theorem OAI.BFSSQuantum.AlgebraData.normal_gap line 145
  9. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.NormalClosedEnergyData.zero_forms line 181
  10. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.NormalClosedEnergyData.exists_nonzero_zero_form line 189