OAI/MathematicalPhysics/BFSS/LowerContinuity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weighted moment and closed normal-form lower semicontinuity.

  1. theorem OAI.BFSSNormalAnalysis.weighted_moment_norm_lsc line 14
  2. lemma OAI.BFSSNormalAnalysis.weighted_moment_sq_lsc line 42
  3. lemma OAI.BFSSSliceSobolev.closedGraph_extract_sequence line 68
  4. theorem OAI.BFSSSliceSobolev.weighted_closed_form_lsc line 89
  5. theorem OAI.BFSSQuantum.AlgebraData.normalForm_lsc line 146