OAI/MathematicalPhysics/BFSS/FormCompactness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Weighted form compactness and confining coercivity.

  1. theorem OAI.BFSSSliceSobolev.core_moment_totallyBounded line 19
  2. lemma OAI.BFSSSliceSobolev.weightedToL2_norm_sq line 74
  3. lemma OAI.BFSSSliceSobolev.weightedClosure_approx line 83
  4. theorem OAI.BFSSSliceSobolev.weightedClosure_totallyBounded line 94
  5. lemma OAI.BFSSNormalAnalysis.constant_quadratic_abs_le line 150
  6. lemma OAI.BFSSNormalAnalysis.constant_quadratic_coercive line 156
  7. lemma OAI.BFSSQuantum.AlgebraData.normalOscillatorForm_weighted line 173
  8. lemma OAI.BFSSQuantum.AlgebraData.normalOscillator_coercive line 183
  9. theorem OAI.BFSSQuantum.AlgebraData.normalForm_totallyBounded line 193