OAI/MathematicalPhysics/BFSS/GaugeGeometry.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Gauge conjugation, exponential curves and nearest normal points.

  1. def OAI.BFSSQuantum.AlgebraData.colorExtract line 13
  2. lemma OAI.BFSSQuantum.AlgebraData.colorExtract_embed line 22
  3. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_extract line 26
  4. def OAI.BFSSQuantum.AlgebraData.colorConjugate line 29
  5. lemma OAI.BFSSQuantum.AlgebraData.colorEmbed_conjugate line 34
  6. lemma OAI.BFSSQuantum.AlgebraData.bracket_conjugate line 43
  7. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_lie line 55
  8. def OAI.BFSSQuantum.AlgebraData.gaugeConjugate line 64
  9. lemma OAI.BFSSQuantum.AlgebraData.spatialColor_gaugeConjugate line 67
  10. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_zeroRelations line 70
  11. lemma OAI.BFSSQuantum.AlgebraData.gaugeConjugate_mem_massiveZeros line 80
  12. lemma OAI.BFSSGaugeFlow.exp_skew line 92
  13. lemma OAI.BFSSGaugeFlow.exp_conj_deriv_zero line 100
  14. lemma OAI.BFSSGaugeFlow.exp_conj_reverse line 108
  15. lemma OAI.BFSSQuantum.AlgebraData.colorExtract_bracket line 123
  16. def OAI.BFSSQuantum.AlgebraData.gaugeCurve line 127
  17. lemma OAI.BFSSQuantum.AlgebraData.gaugeCurve_mem_massiveZeros line 130
  18. lemma OAI.BFSSQuantum.AlgebraData.gaugeCurve_zero line 135
  19. lemma OAI.BFSSQuantum.AlgebraData.colorConjugate_curve_deriv line 144
  20. def OAI.BFSSQuantum.AlgebraData.bosonAssemble line 160
  21. lemma OAI.BFSSQuantum.AlgebraData.gaugeCurve_deriv_zero line 165
  22. theorem OAI.BFSSQuantum.AlgebraData.nearest_zero_normal line 173