OAI/MathematicalPhysics/BFSS/Cutoffs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite IMS identities and exact smooth cutoff energy decompositions.

  1. lemma OAI.BFSSQuantum.AlgebraData.finite_ims_algebra line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.cutoffGradient_partition line 27
  3. lemma OAI.BFSSQuantum.AlgebraData.charge_ims_pointwise line 50
  4. lemma OAI.BFSSQuantum.AlgebraData.coreToL2_norm_sq line 85
  5. lemma OAI.BFSSQuantum.AlgebraData.coreNormSq_integrable line 93
  6. lemma OAI.BFSSQuantum.AlgebraData.cutoffGradient_continuous line 98
  7. lemma OAI.BFSSQuantum.AlgebraData.cutoffError_integrable line 106
  8. lemma OAI.BFSSQuantum.AlgebraData.charge_ims line 119
  9. lemma OAI.BFSSQuantum.AlgebraData.coreForm_ims line 137