OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/ClassicalTensor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

C1 tensor products and their actual weak-H1 partials. Fubini supplies L2 membership for decaying orbitals; compact support is unnecessary.

  1. theorem OAI.ContinuumCoulomb.tensorOrbital_C1 line 14
  2. theorem OAI.ContinuumCoulomb.tensorOrbital_C1_fderiv line 22
  3. theorem OAI.ContinuumCoulomb.tensorOrbital_partial_memLp line 50