OAI/MathematicalPhysics/BFSS/ProfileEnergy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Profile integral identities and ambient-to-normal energy comparison.

  1. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.local_density_integral line 16
  2. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredField_fermionic line 50
  3. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_fermionic_integral line 77
  4. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_bosonic_integral line 99
  5. def OAI.BFSSQuantum.AlgebraData.coreEnergyDensity line 129
  6. lemma OAI.BFSSQuantum.AlgebraData.coreEnergyDensity_continuous line 132
  7. lemma OAI.BFSSQuantum.AlgebraData.coreEnergyDensity_compactSupport line 137
  8. lemma OAI.BFSSQuantum.AlgebraData.coreEnergyDensity_integral line 142
  9. lemma OAI.BFSSQuantum.AlgebraData.coreEnergyDensity_uniform_lower line 152
  10. lemma OAI.BFSSQuantum.AlgebraData.cutoff_energy_le line 164
  11. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.ambientEnergy line 201
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.ambientEnergy_eq line 204
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.ambientEnergy_profile_eq line 227
  14. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalPatch_energy_comparison line 246