OAI/MathematicalPhysics/BFSS/NormalTubes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Normal chord estimates, reach and unique tube fibers.

  1. lemma OAI.BFSSQuantum.AlgebraData.bracketLinearization_gaugeTangent line 13
  2. lemma OAI.BFSSQuantum.AlgebraData.cyclicLinearization_gaugeTangent line 22
  3. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_sub_tangent line 32
  4. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_projection line 79
  5. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_normal_chord line 88
  6. lemma OAI.BFSSQuantum.AlgebraData.normal_pairing_chord line 121
  7. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_normal_reach line 134
  8. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_normal_tubes line 171
  9. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_add line 203
  10. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_smul line 210
  11. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_norm line 217
  12. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_tube_fiber line 224
  13. theorem OAI.BFSSQuantum.AlgebraData.massiveDistance_normal_tube line 253