OAI/MathematicalPhysics/BFSS/MixedEnergy.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Mixed first-order differential and potential energy identities.

  1. def OAI.BFSSQuantum.AlgebraData.kineticComplexSymbol line 14
  2. lemma OAI.BFSSQuantum.AlgebraData.kineticComplexSymbol_apply line 18
  3. lemma OAI.BFSSQuantum.AlgebraData.kineticComplexSymbol_selfAdjoint line 21
  4. lemma OAI.BFSSQuantum.AlgebraData.principalCoefficients_coordinate line 24
  5. lemma OAI.BFSSQuantum.AlgebraData.deformed_mixed_anticommutator line 31
  6. lemma OAI.BFSSQuantum.AlgebraData.deformedPotentialCoefficients_contDiff line 51
  7. lemma OAI.BFSSQuantum.AlgebraData.deformedPotentialMultiplier_contDiff line 59
  8. abbrev OAI.MixedEnergy.E line 75
  9. abbrev OAI.MixedEnergy.Core line 76
  10. def OAI.MixedEnergy.toL2 line 78
  11. lemma OAI.MixedEnergy.toL2_ae line 84
  12. lemma OAI.MixedEnergy.toL2_inner line 89
  13. lemma OAI.MixedEnergy.inner_integrable line 97
  14. def OAI.MixedEnergy.delta line 102
  15. lemma OAI.MixedEnergy.delta_apply line 106
  16. lemma OAI.MixedEnergy.delta_skew line 112
  17. def OAI.MixedEnergy.field line 123
  18. lemma OAI.MixedEnergy.field_apply line 139
  19. lemma OAI.MixedEnergy.delta_field line 145
  20. def OAI.MixedEnergy.post line 156
  21. lemma OAI.MixedEnergy.post_apply line 160
  22. lemma OAI.MixedEnergy.delta_post line 164
  23. lemma OAI.MixedEnergy.post_skew line 176
  24. def OAI.MixedEnergy.firstOrder line 185
  25. lemma OAI.MixedEnergy.firstOrder_apply line 189
  26. lemma OAI.MixedEnergy.firstOrder_symmetric line 194
  27. lemma OAI.MixedEnergy.field_symmetric line 208
  28. lemma OAI.MixedEnergy.mixed_core_identity line 218
  29. def OAI.MixedEnergy.remainderField line 233
  30. def OAI.MixedEnergy.remainderCore line 237
  31. lemma OAI.MixedEnergy.remainderCore_apply line 243
  32. lemma OAI.MixedEnergy.averaged_energy_identity line 272