OAI/MathematicalPhysics/BFSS/OscillatorLimits.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Closed normal oscillator forms and summed profile energy limits.

  1. lemma OAI.BFSSNormalAnalysis.finite_nonnegative_energy_subsequence line 15
  2. abbrev OAI.BFSSQuantum.AlgebraData.NormalGradient line 36
  3. def OAI.BFSSQuantum.AlgebraData.normalOscillatorForm line 40
  4. def OAI.BFSSQuantum.AlgebraData.NormalFormDomain line 47
  5. lemma OAI.BFSSQuantum.AlgebraData.normalPotential_norm_sq line 55
  6. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.ambientKinetic line 79
  7. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profileBosonicEnergy line 82
  8. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profileFermionicEnergy line 86
  9. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.ambientKinetic_nonneg line 90
  10. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profileBosonicEnergy_nonneg line 93
  11. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.ambientEnergy_components line 96
  12. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_oscillator_le_limits line 102
  13. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalPatch_summed_energy_limit line 136
  14. lemma OAI.BFSSQuantum.jointEnergy_distance_le line 218