OAI/MathematicalPhysics/BFSS/FiniteFamilies.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Joint energy, closed-profile norm exhaustion and finite-family limits.

  1. def OAI.BFSSQuantum.jointEnergy line 12
  2. lemma OAI.BFSSQuantum.jointEnergy_continuous line 15
  3. lemma OAI.BFSSQuantum.jointEnergy_nonneg line 19
  4. lemma OAI.BFSSQuantum.AlgebraData.jointEnergy_core line 24
  5. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.deformedModelGraph_closure_subtype line 32
  6. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.normalPatch_closedSet line 45
  7. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.normalPatch_bound_closed line 59
  8. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalClosed_norm_exhaustion line 83
  9. lemma OAI.BFSSRellich.totallyBounded_asymptotic line 124
  10. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile_totallyBounded line 147
  11. lemma OAI.BFSSQuantum.jointEnergy_le line 198
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.normalFamily_normlimit line 212
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.graph_linearCombination line 252
  14. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.linearCombination_norm_le line 263
  15. def OAI.BFSSQuantum.AlgebraData.GaugeData.NormalFamilyConclusion line 273
  16. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalClosed_finiteFamily line 288