OAI/MathematicalPhysics/BFSS/OrbitDensity.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Stabilizer-invariant normal density and orbit measures.

  1. def OAI.BFSSQuantum.AlgebraData.stabilizerNormalIsometry line 16
  2. lemma OAI.BFSSQuantum.AlgebraData.stabilizerNormalIsometry_one line 30
  3. lemma OAI.BFSSQuantum.AlgebraData.stabilizerNormalIsometry_mul line 33
  4. lemma OAI.BFSSQuantum.AlgebraData.stabilizerNormalIsometry_continuous line 40
  5. def OAI.BFSSQuantum.AlgebraData.stabilizerPositiveCompact line 50
  6. def OAI.BFSSQuantum.AlgebraData.stabilizerHaar line 57
  7. instance OAI.BFSSQuantum.AlgebraData.stabilizerHaar_isHaar line 60
  8. instance OAI.BFSSQuantum.AlgebraData.stabilizerHaar_isProbability line 64
  9. def OAI.BFSSQuantum.AlgebraData.normalInvariantDensity line 68
  10. lemma OAI.BFSSQuantum.AlgebraData.normalInvariantDensity_zero line 72
  11. lemma OAI.BFSSQuantum.AlgebraData.normalInvariantDensity_nonneg line 76
  12. lemma OAI.BFSSQuantum.AlgebraData.normalInvariantDensity_continuous line 80
  13. lemma OAI.BFSSQuantum.AlgebraData.normalInvariantDensity_invariant line 91
  14. theorem OAI.BFSSQuantum.AlgebraData.normalInvariantDensity_integral line 110
  15. lemma OAI.BFSSQuantum.AlgebraData.normalAffine_isometry line 158
  16. lemma OAI.BFSSQuantum.AlgebraData.normalAffine_compactSupport line 164
  17. theorem OAI.BFSSQuantum.AlgebraData.normalOrbit_measure line 169