OAI/MathematicalPhysics/BFSS/NormalLinearization.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Gauge tangent slices, normal coercivity and Taylor squares.

  1. def OAI.BFSSQuantum.AlgebraData.spatialColorMap line 13
  2. def OAI.BFSSQuantum.AlgebraData.gaugeTangent line 18
  3. def OAI.BFSSQuantum.AlgebraData.normalSlice line 27
  4. lemma OAI.BFSSQuantum.AlgebraData.spatialColor_gaugeTangent line 30
  5. lemma OAI.BFSSQuantum.AlgebraData.spatialColor_inner line 33
  6. lemma OAI.BFSSQuantum.AlgebraData.gaugeTangent_pairing line 38
  7. lemma OAI.BFSSQuantum.AlgebraData.mem_normalSlice_iff line 47
  8. lemma OAI.BFSSQuantum.AlgebraData.bracketLinearization_eq line 59
  9. def OAI.BFSSQuantum.AlgebraData.bracketLinearizationMap line 67
  10. lemma OAI.BFSSQuantum.AlgebraData.bracketLinearizationMap_apply line 71
  11. def OAI.BFSSQuantum.AlgebraData.cyclicLinearizationMap line 75
  12. lemma OAI.BFSSQuantum.AlgebraData.cyclicLinearizationMap_apply line 78
  13. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_continuous line 84
  14. lemma OAI.BFSSQuantum.AlgebraData.normalQuadratic_smul line 104
  15. theorem OAI.BFSSQuantum.AlgebraData.normalQuadratic_coercive line 115
  16. lemma OAI.BFSSQuantum.AlgebraData.colorLie_continuous line 138
  17. lemma OAI.BFSSQuantum.AlgebraData.spatialBracket_continuous line 147
  18. lemma OAI.BFSSQuantum.AlgebraData.potential_color line 152
  19. lemma OAI.BFSSQuantum.AlgebraData.cyclicResidual_continuous line 192
  20. lemma OAI.BFSSQuantum.AlgebraData.potential_continuous line 203
  21. lemma OAI.BFSSQuantum.AlgebraData.potential_nonneg line 220
  22. lemma OAI.BFSSQuantum.AlgebraData.potential_zero_of_relations line 224
  23. lemma OAI.BFSSQuantum.AlgebraData.bracket_taylor line 245
  24. lemma OAI.BFSSQuantum.AlgebraData.cyclic_taylor line 252
  25. theorem OAI.BFSSQuantum.AlgebraData.potential_taylor_squares line 260