OAI/MathematicalPhysics/BFSS/NormalCharts.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Exponential normal charts, derivatives, Jacobians and local integration.

  1. lemma OAI.BFSSSlice.exp_linear_strictFDeriv_zero line 15
  2. def OAI.BFSSSlice.conjugationDifferential line 22
  3. lemma OAI.BFSSSlice.conjugationDifferential_apply line 28
  4. lemma OAI.BFSSSlice.exp_conj_strictFDeriv_zero line 32
  5. def OAI.BFSSQuantum.AlgebraData.gaugeTangentLift line 52
  6. lemma OAI.BFSSQuantum.AlgebraData.gaugeTangentLift_right line 56
  7. abbrev OAI.BFSSQuantum.AlgebraData.SliceParameter line 62
  8. def OAI.BFSSQuantum.AlgebraData.sliceLinearEquiv line 65
  9. lemma OAI.BFSSQuantum.AlgebraData.sliceLinearEquiv_apply line 69
  10. def OAI.BFSSQuantum.AlgebraData.sliceGaugeLift line 72
  11. def OAI.BFSSQuantum.AlgebraData.sliceNormalTranslation line 75
  12. def OAI.BFSSQuantum.AlgebraData.sliceGaugeGenerator line 78
  13. lemma OAI.BFSSQuantum.AlgebraData.sliceGaugeGenerator_apply line 81
  14. def OAI.BFSSQuantum.AlgebraData.normalChartMap line 84
  15. lemma OAI.BFSSQuantum.AlgebraData.normalChartMap_zero line 87
  16. lemma OAI.BFSSQuantum.AlgebraData.gaugeExponential_star line 90
  17. lemma OAI.BFSSQuantum.AlgebraData.gaugeExponential_unitary line 96
  18. def OAI.BFSSQuantum.AlgebraData.sliceSpatialTranslation line 101
  19. lemma OAI.BFSSQuantum.AlgebraData.normalChartMap_spatial line 106
  20. lemma OAI.BFSSQuantum.AlgebraData.slice_spatial_differential line 119
  21. lemma OAI.BFSSQuantum.AlgebraData.normalChart_spatial_strictFDeriv line 143
  22. lemma OAI.BFSSQuantum.AlgebraData.normalChartMap_strictFDeriv line 172
  23. def OAI.BFSSQuantum.AlgebraData.normalLocalChart line 183
  24. lemma OAI.BFSSQuantum.AlgebraData.normalLocalChart_coe line 186
  25. lemma OAI.BFSSQuantum.AlgebraData.normalLocalChart_source line 189
  26. lemma OAI.BFSSQuantum.AlgebraData.normalLocalChart_target line 192
  27. lemma OAI.BFSSQuantum.AlgebraData.normalLocalChart_inverse line 197
  28. lemma OAI.BFSSQuantum.AlgebraData.normalChartMap_contDiff line 209
  29. def OAI.BFSSQuantum.AlgebraData.normalEuclideanChart line 231
  30. lemma OAI.BFSSQuantum.AlgebraData.normalEuclideanChart_contDiff line 234
  31. lemma OAI.BFSSQuantum.AlgebraData.normalEuclideanChart_zero line 238
  32. lemma OAI.BFSSQuantum.AlgebraData.normalEuclideanChart_strictFDeriv_zero line 241
  33. def OAI.BFSSQuantum.AlgebraData.normalChartJacobian line 253
  34. lemma OAI.BFSSQuantum.AlgebraData.normalChartJacobian_continuous line 256
  35. lemma OAI.BFSSQuantum.AlgebraData.normalChartJacobian_zero line 261
  36. theorem OAI.BFSSQuantum.AlgebraData.normalChart_local_integral line 265
  37. lemma OAI.BFSSQuantum.AlgebraData.sliceLinearEquiv_measurePreserving line 305
  38. lemma OAI.BFSSQuantum.AlgebraData.normalChartMap_invariant line 315