OAI/MathematicalPhysics/BFSS/EnergyExtraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Strong core and closed energy extraction with lower limits.

  1. structure OAI.BFSSQuantum.AlgebraData.GaugeData.NormalCoreEnergyData line 15
  2. def OAI.BFSSQuantum.AlgebraData.GaugeData.NormalCoreEnergyConclusion line 32
  3. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalCore_energy_extraction line 35
  4. structure OAI.BFSSQuantum.AlgebraData.GaugeData.NormalClosedEnergyData line 96
  5. def OAI.BFSSQuantum.AlgebraData.GaugeData.NormalClosedEnergyConclusion line 113
  6. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalClosed_energy_extraction line 116
  7. lemma OAI.BFSSNormalAnalysis.nonnegative_bounded_liminf_subsequence line 194
  8. lemma OAI.BFSSQuantum.charge_norm_bound_of_energy line 217
  9. def OAI.BFSSQuantum.AlgebraData.GaugeData.NormalClosedEnergyData.reindex line 236
  10. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalClosed_liminf_extraction line 255