OAI/MathematicalPhysics/BFSS/SliceDensity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Positive continuous slice density and scaled measures.

  1. lemma OAI.BFSSQuantum.AlgebraData.normalPatchDensity_nonneg line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.normalPatchDensity_compact line 19
  3. lemma OAI.BFSSQuantum.AlgebraData.normalPatchDensity_continuous line 32
  4. lemma OAI.BFSSQuantum.AlgebraData.normalSliceDensity_continuous line 53
  5. lemma OAI.BFSSQuantum.AlgebraData.normalSliceDensity_nonneg line 78
  6. lemma OAI.BFSSQuantum.AlgebraData.normalSliceDensity_pos_zero line 83
  7. theorem OAI.BFSSQuantum.AlgebraData.normalSlice_measure_exists line 117
  8. def OAI.BFSSQuantum.AlgebraData.orbitDimension line 154
  9. lemma OAI.BFSSQuantum.AlgebraData.orbitDimension_add_normalDimension line 156
  10. theorem OAI.BFSSQuantum.AlgebraData.normalSlice_scaled_measure line 160