OAI/MathematicalPhysics/BFSS/DistanceBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Uniform potential and energy bounds by distance to the zero set.

  1. lemma OAI.BFSSQuantum.AlgebraData.potential_uniform_normal_lower line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.nearest_massive_zero line 37
  3. lemma OAI.BFSSQuantum.AlgebraData.infDist_massiveZeros_le_norm line 48
  4. theorem OAI.BFSSQuantum.AlgebraData.potential_global_distance_lower line 52
  5. def OAI.BFSSQuantum.AlgebraData.massiveDistance line 116
  6. lemma OAI.BFSSQuantum.AlgebraData.massiveDistance_continuous line 119
  7. lemma OAI.BFSSQuantum.AlgebraData.massiveDistance_nonneg line 122
  8. lemma OAI.BFSSQuantum.AlgebraData.massiveDistance_rescale line 125
  9. theorem OAI.BFSSQuantum.AlgebraData.potential_uniform_distance line 132
  10. lemma OAI.BFSSQuantum.AlgebraData.massiveDistance_scaled_norm line 148
  11. theorem OAI.BFSSQuantum.AlgebraData.deformedPotential_fermion_uniform_distance line 161
  12. theorem OAI.BFSSQuantum.AlgebraData.massive_core_uniform_distance line 199