OAI/MathematicalPhysics/BFSS/GaugeOrbits.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Compact gauge orbits, stabilizers and equivariant normal slices.

  1. lemma OAI.BFSSOrbit.unitary_compact line 12
  2. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_one line 26
  3. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_mul line 30
  4. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_one line 37
  5. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_mul line 43
  6. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_continuous line 50
  7. def OAI.BFSSQuantum.AlgebraData.gaugeOrbit line 58
  8. lemma OAI.BFSSQuantum.AlgebraData.self_mem_gaugeOrbit line 61
  9. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_isCompact line 64
  10. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_subset_massiveZeros line 67
  11. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_invariant line 72
  12. lemma OAI.BFSSQuantum.AlgebraData.gaugeCurve_mem_gaugeOrbit line 78
  13. lemma OAI.BFSSQuantum.AlgebraData.nearest_gaugeOrbit_normal line 83
  14. lemma OAI.BFSSQuantum.AlgebraData.nearest_gaugeOrbit line 100
  15. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_locally_single_orbit line 112
  16. theorem OAI.BFSSQuantum.AlgebraData.massiveZeros_finite_orbits line 133
  17. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_inner line 155
  18. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_inner line 168
  19. def OAI.BFSSQuantum.AlgebraData.gaugeAction line 175
  20. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_one line 177
  21. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_mul line 179
  22. lemma OAI.BFSSQuantum.AlgebraData.gaugeAction_inv line 182
  23. def OAI.BFSSQuantum.AlgebraData.gaugeStabilizer line 186
  24. lemma OAI.BFSSQuantum.AlgebraData.mem_gaugeStabilizer line 197
  25. lemma OAI.BFSSQuantum.AlgebraData.gaugeStabilizer_isClosed line 200
  26. lemma OAI.BFSSQuantum.AlgebraData.gaugeStabilizer_isCompact line 204
  27. lemma OAI.BFSSQuantum.AlgebraData.gaugeOrbit_fiber line 210
  28. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_linear line 221
  29. lemma OAI.BFSSQuantum.AlgebraData.gaugeTangent_equivariant line 235
  30. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_inverse line 245
  31. lemma OAI.BFSSQuantum.AlgebraData.normalSlice_equivariant line 250
  32. lemma OAI.BFSSQuantum.AlgebraData.stabilizer_preserves_normalSlice line 260