OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/TensorDifferential.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate derivatives of tensor products. Cross-coordinate factors remain constant when differentiating a second time in one slot.

  1. def OAI.ContinuumCoulomb.coordinateProduct line 13
  2. def OAI.ContinuumCoulomb.positionComplexPartial line 16
  3. def OAI.ContinuumCoulomb.positionComplexLaplacian line 19
  4. theorem OAI.ContinuumCoulomb.coordinateProduct_C1 line 22
  5. theorem OAI.ContinuumCoulomb.coordinateProduct_C2 line 28
  6. theorem OAI.ContinuumCoulomb.coordinateProduct_partial line 34
  7. theorem OAI.ContinuumCoulomb.coordinateProduct_partial_product line 42
  8. theorem OAI.ContinuumCoulomb.positionComplexPartial_C1 line 53
  9. theorem OAI.ContinuumCoulomb.coordinateProduct_second line 57
  10. theorem OAI.ContinuumCoulomb.coordinateProduct_laplacian line 77