OAI/MathematicalPhysics/BFSS/PotentialBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Fermion multiplier growth and global deformed potential scaling.

  1. def OAI.BFSSQuantum.AlgebraData.bracketBilinear line 22
  2. def OAI.BFSSQuantum.AlgebraData.massLinear line 31
  3. lemma OAI.BFSSQuantum.AlgebraData.deformedRealField_polarized line 37
  4. lemma OAI.BFSSQuantum.AlgebraData.deformedRealField_derivative_bound line 71
  5. def OAI.BFSSQuantum.AlgebraData.fermionGrowthConstant line 96
  6. lemma OAI.BFSSQuantum.AlgebraData.fermionGrowthConstant_nonneg line 100
  7. lemma OAI.BFSSQuantum.AlgebraData.deformedFermionField_growth line 104
  8. lemma OAI.BFSSQuantum.AlgebraData.deformedFermionField_inner_lower line 136
  9. def OAI.BFSS.scaleConfiguration line 158
  10. lemma OAI.BFSS.configurationNormSq_scale line 162
  11. lemma OAI.BFSS.massive_potential_scaling line 166
  12. lemma OAI.BFSSQuantum.AlgebraData.matrixConfiguration_smul line 211
  13. lemma OAI.BFSSQuantum.AlgebraData.deformedBosonicPotential_scaling line 220
  14. lemma OAI.BFSSQuantum.AlgebraData.deformedBosonicPotential_nonneg line 226
  15. theorem OAI.BFSSQuantum.AlgebraData.deformedBosonicPotential_global line 231