OAI/MathematicalPhysics/BFSS/ProfileMoments.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Closed weighted moments and basis-independent slice kinetic bounds.

  1. theorem OAI.BFSSNormalAnalysis.weighted_moment_closed line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_moment_mem line 46
  3. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_moment_norm_sq line 57
  4. theorem OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_limit_moment line 65
  5. lemma OAI.BFSSSliceAnalytic.orthonormal_kinetic_le line 113
  6. lemma OAI.BFSSSliceAnalytic.kinetic_basis_independent line 131
  7. lemma OAI.BFSSSliceAnalytic.slice_kinetic_le line 137
  8. lemma OAI.BFSSSliceAnalytic.affine_kinetic_le line 142