OAI/MathematicalPhysics/BFSS/FormClosure.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Weighted Sobolev form closure and normal oscillator nonnegativity.

  1. def OAI.BFSSSliceSobolev.weightedToL2 line 17
  2. lemma OAI.BFSSSliceSobolev.weightedToL2_ae line 22
  3. def OAI.BFSSSliceSobolev.weightedClosure line 25
  4. def OAI.BFSSSliceSobolev.coreMul line 30
  5. lemma OAI.BFSSSliceSobolev.coreMul_apply line 35
  6. lemma OAI.BFSSSliceSobolev.coreMul_derivative line 39
  7. abbrev OAI.BFSSSliceSobolev.scalarMul line 49
  8. def OAI.BFSSSliceSobolev.cutoffGradient line 52
  9. def OAI.BFSSSliceSobolev.cutoffMoment line 56
  10. lemma OAI.BFSSSliceSobolev.cutoffGradient_continuous line 60
  11. lemma OAI.BFSSSliceSobolev.cutoff_core_tuple line 70
  12. lemma OAI.BFSSSliceSobolev.cutoff_mem_weightedClosure line 101
  13. def OAI.BFSSSliceSobolev.bumpCore line 129
  14. lemma OAI.BFSSSliceSobolev.bumpCore_apply line 134
  15. lemma OAI.BFSSSliceSobolev.bumpCore_derivative line 138
  16. lemma OAI.BFSSSliceSobolev.scalarMul_bump_tendsto line 148
  17. lemma OAI.BFSSSliceSobolev.scalarMul_bump_derivative_tendsto line 171
  18. lemma OAI.BFSSSliceSobolev.cutoffGradient_bump_tendsto line 193
  19. lemma OAI.BFSSSliceSobolev.cutoffMoment_eq_scalarMul line 206
  20. theorem OAI.BFSSSliceSobolev.mem_weightedClosure line 218
  21. def OAI.BFSSQuantum.AlgebraData.normalMomentWeight line 247
  22. lemma OAI.BFSSQuantum.AlgebraData.normalMomentWeight_continuous line 250
  23. lemma OAI.BFSSQuantum.AlgebraData.normalWeightedCore_norm_sq line 254
  24. theorem OAI.BFSSQuantum.AlgebraData.normalOscillator_nonneg line 265