OAI/MathematicalPhysics/BFSS/GaugeCore.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Gauge actions on the physical Hilbert space and invariant smooth core.

  1. def OAI.BFSSQuantum.AlgebraData.adjointCoefficient line 14
  2. structure OAI.BFSSQuantum.AlgebraData.GaugeData line 18
  3. def OAI.BFSSQuantum.AlgebraData.GaugeData.bosonPullback line 32
  4. def OAI.BFSSQuantum.AlgebraData.GaugeData.fiberAction line 35
  5. def OAI.BFSSQuantum.AlgebraData.GaugeData.physicalSpace line 39
  6. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.physicalSpace_closed line 42
  7. def OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore line 52
  8. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_equivariant line 55
  9. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_norm_gauge line 75
  10. lemma OAI.BFSSQuantum.AlgebraData.exists_specialUnitary_same_conjugation line 90
  11. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.boson_eq_gaugeAction line 120
  12. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.unitary_boson_exists line 132
  13. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_norm_unitary line 144
  14. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_fderiv line 160
  15. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_fderiv_norm line 176
  16. lemma OAI.BFSSQuantum.AlgebraData.GaugeData.invariantCore_fderiv_norm_unitary line 191