OAI/MathematicalPhysics/BFSS/ProfileExtraction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Normal coordinate profiles and strong core extraction.

  1. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateField_compactSupport line 15
  2. def OAI.BFSSQuantum.AlgebraData.normalCoordinateWeight line 21
  3. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinateWeight_continuous line 25
  4. def OAI.BFSSQuantum.AlgebraData.normalMeasuredCoordinates line 32
  5. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredCoordinates_eq line 36
  6. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredCoordinates_continuous line 43
  7. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredCoordinates_compactSupport line 50
  8. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredCoordinates_norm_integral line 56
  9. lemma OAI.BFSSQuantum.AlgebraData.normalMeasuredCoordinates_moment_integral line 65
  10. def OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile line 85
  11. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_norm_square line 91
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_norm_eq line 95
  13. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_totallyBounded line 99
  14. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.normalCore_extraction line 145