OAI/MathematicalPhysics/BFSS/SliceIntegrals.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Slice densities and compact gauge Haar measures.

  1. def OAI.BFSSQuantum.AlgebraData.normalPatchDensity line 15
  2. def OAI.BFSSQuantum.AlgebraData.normalSliceDensity line 20
  3. lemma OAI.BFSSQuantum.AlgebraData.normalEuclideanChart_sliceLinearEquiv line 24
  4. theorem OAI.BFSSQuantum.AlgebraData.normalPatch_integral line 28
  5. lemma OAI.BFSSQuantum.AlgebraData.normalPatch_integrable line 61
  6. theorem OAI.BFSSQuantum.AlgebraData.normalSlice_integral line 89
  7. def OAI.BFSSQuantum.AlgebraData.gaugeIsometry line 116
  8. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_measurePreserving line 126
  9. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_continuous line 130
  10. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_image_zeros line 145
  11. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_infDist line 154
  12. def OAI.BFSSQuantum.AlgebraData.gaugePositiveCompact line 160
  13. def OAI.BFSSQuantum.AlgebraData.gaugeHaar line 168
  14. instance OAI.BFSSQuantum.AlgebraData.gaugeHaar_isHaar line 171
  15. instance OAI.BFSSQuantum.AlgebraData.gaugeHaar_isProbability line 174
  16. def OAI.BFSSQuantum.AlgebraData.gaugeOrbitMeasure line 179
  17. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbitMap_continuous line 182
  18. instance OAI.BFSSQuantum.AlgebraData.gaugeOrbitMeasure_isProbability line 189
  19. lemma OAI.BFSSQuantum.AlgebraData.gauge_average_on_orbit line 194