OAI/MathematicalPhysics/BFSS/TaylorBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Uniform Taylor remainders and compact massive zero sets.

  1. lemma OAI.BFSSNormal.quartic_upper line 12
  2. lemma OAI.BFSSNormal.norm_add_square_lower line 45
  3. lemma OAI.BFSSNormal.sum_square_lower line 51
  4. def OAI.BFSSQuantum.AlgebraData.quarticRemainder line 70
  5. lemma OAI.BFSSQuantum.AlgebraData.quarticRemainder_continuous line 77
  6. lemma OAI.BFSSQuantum.AlgebraData.quarticRemainder_smul line 87
  7. lemma OAI.BFSSQuantum.AlgebraData.quarticRemainder_bound line 103
  8. theorem OAI.BFSSQuantum.AlgebraData.potential_taylor_lower line 108
  9. def OAI.BFSSQuantum.AlgebraData.massiveZeros line 137
  10. lemma OAI.BFSSQuantum.AlgebraData.zero_mem_massiveZeros line 139
  11. lemma OAI.BFSSQuantum.AlgebraData.massiveZeros_isClosed line 145
  12. lemma OAI.BFSSQuantum.AlgebraData.massiveZeros_isCompact line 148
  13. lemma OAI.BFSSQuantum.AlgebraData.bracketLinearization_jointContinuous line 161
  14. lemma OAI.BFSSQuantum.AlgebraData.cyclicLinearization_jointContinuous line 170
  15. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_jointContinuous line 178
  16. lemma OAI.BFSSQuantum.AlgebraData.gaugeDivergence_jointContinuous line 195
  17. theorem OAI.BFSSQuantum.AlgebraData.normalQuadratic_uniform_coercive line 206