OAI/MathematicalPhysics/BFSS/PotentialSquares.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Shifted potential squares, coercivity and odd gamma traces.

  1. lemma OAI.BFSSGamma.shiftedPair_squares line 13
  2. lemma OAI.BFSSGamma.spatialTail_sum line 63
  3. lemma OAI.BFSSGamma.tailIndex_sum line 79
  4. lemma OAI.BFSSQuantum.AlgebraData.deformedBosonicPotential_matrix line 95
  5. theorem OAI.BFSSQuantum.AlgebraData.deformedBosonicPotential_coercive line 146
  6. lemma OAI.BFSSGamma.trace_list_odd line 168
  7. lemma OAI.BFSSGamma.gamma_pair_trace_zero line 193
  8. lemma OAI.BFSSGamma.gamma_mass_trace_zero line 200
  9. lemma OAI.BFSSGamma.gamma_bracketMass_trace_zero line 207