OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/FiniteTensorState.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite products of the actual smooth orbitals lie in the full H1 domain. Their synthesis agrees with the orthogonal L2 tensor synthesis.

  1. def OAI.ContinuumCoulomb.classicalTensorState line 15
  2. def OAI.ContinuumCoulomb.finiteTensorState line 25
  3. theorem OAI.ContinuumCoulomb.finiteTensorState_toHilbert line 34
  4. def OAI.ContinuumCoulomb.finiteTensorProjection line 49
  5. theorem OAI.ContinuumCoulomb.finiteTensorProjection_toHilbert line 57
  6. theorem OAI.ContinuumCoulomb.finiteTensorProjection_coefficients line 69