OAI/MathematicalPhysics/BFSS/StabilizerProfiles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Stabilizer-equivariant normal profile spaces and limits.

  1. def OAI.BFSSQuantum.AlgebraData.stabilizerCoordinateIsometry line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.normalCoordinate_stabilizer line 19
  3. def OAI.BFSSQuantum.AlgebraData.GaugeData.stabilizerOfGauge line 29
  4. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.fermion_real_smul line 34
  5. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.normalCoreField_equivariant line 38
  6. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.normalMeasuredField_equivariant line 52
  7. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.normalMeasuredCoordinates_equivariant line 67
  8. def OAI.BFSSQuantum.AlgebraData.GaugeData.normalBosonPullback line 84
  9. def OAI.BFSSQuantum.AlgebraData.GaugeData.normalFiberAction line 90
  10. def OAI.BFSSQuantum.AlgebraData.GaugeData.normalEquivariantSpace line 95
  11. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.normalEquivariantSpace_closed line 100
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.profile_mem_equivariantSpace line 116
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.closedProfile_mem_equivariantSpace line 138
  14. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.MeasuredNormalPatch.limit_mem_equivariantSpace line 148