OAI/MathematicalPhysics/BFSS/Kinetic.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Constant-coefficient kinetic identities and local gradient bounds.

  1. abbrev OAI.BFSSKinetic.E line 13
  2. abbrev OAI.BFSSKinetic.Core line 14
  3. def OAI.BFSSKinetic.delta line 16
  4. def OAI.BFSSKinetic.post line 19
  5. lemma OAI.BFSSKinetic.post_apply line 23
  6. lemma OAI.BFSSKinetic.delta_apply line 27
  7. lemma OAI.BFSSKinetic.delta_post line 34
  8. lemma OAI.BFSSKinetic.delta_delta line 44
  9. def OAI.BFSSKinetic.toL2 line 62
  10. lemma OAI.BFSSKinetic.toL2_ae line 68
  11. lemma OAI.BFSSKinetic.inner_integrable line 73
  12. lemma OAI.BFSSKinetic.toL2_inner line 79
  13. lemma OAI.BFSSKinetic.delta_skew line 87
  14. lemma OAI.BFSSKinetic.post_symmetric line 100
  15. def OAI.BFSSKinetic.kineticDerivative line 110
  16. lemma OAI.BFSSKinetic.kineticDerivative_apply line 114
  17. lemma OAI.BFSSKinetic.kineticDerivative_skew line 118
  18. lemma OAI.BFSSKinetic.post_mul line 128
  19. lemma OAI.BFSSKinetic.post_add line 134
  20. lemma OAI.BFSSKinetic.kineticDerivative_twice_expand line 140
  21. lemma OAI.BFSSKinetic.kineticDerivative_twice line 147
  22. lemma OAI.BFSSKinetic.kinetic_norm_sq line 171
  23. lemma OAI.BFSSQuantum.AlgebraData.principalSymbol_basis_mixed line 196
  24. def OAI.BFSSQuantum.AlgebraData.kineticSymbol line 220
  25. lemma OAI.BFSSQuantum.AlgebraData.kineticSymbol_selfAdjoint line 224
  26. lemma OAI.BFSSQuantum.AlgebraData.kineticSymbol_CAR line 233
  27. lemma OAI.BFSSQuantum.AlgebraData.literal_kinetic_norm line 246
  28. def OAI.BFSSQuantum.AlgebraData.bracketMultiplier line 261
  29. lemma OAI.BFSSQuantum.AlgebraData.bracketMultiplier_continuous line 267
  30. lemma OAI.BFSSQuantum.AlgebraData.kineticSymbol_apply line 271
  31. lemma OAI.BFSSQuantum.AlgebraData.kineticDerivative_pointwise line 278
  32. lemma OAI.BFSSQuantum.AlgebraData.charge_kinetic_plus_bracket line 287
  33. def OAI.BFSSQuantum.AlgebraData.bracketPart line 294
  34. lemma OAI.BFSSQuantum.AlgebraData.bracketPart_apply line 297
  35. lemma OAI.BFSSQuantum.AlgebraData.bracketPart_bound line 303
  36. lemma OAI.BFSSQuantum.AlgebraData.kinetic_norm_le_charge_add_bracket line 315
  37. lemma OAI.BFSSQuantum.AlgebraData.gradient_bound_of_kinetic_bound line 331
  38. lemma OAI.BFSSQuantum.AlgebraData.compact_bracket_bound line 340
  39. theorem OAI.BFSSQuantum.AlgebraData.local_gradient_bound line 347