OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/OrbitalDerivative.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual L2 derivative-slot tensors and their exact kinetic matrix compression to CAR one-body operators. Derivative families are concrete functions with L2 hypotheses, so spatial partial derivatives can be used directly without assuming a kinetic-energy matrix identity.

  1. lemma OAI.ContinuumCoulomb.OrbitalDerivative.basisTensor_substitution line 16
  2. def OAI.ContinuumCoulomb.OrbitalDerivative.derivativeTensorValue line 29
  3. def OAI.ContinuumCoulomb.OrbitalDerivative.normalizedSlotWave line 34
  4. lemma OAI.ContinuumCoulomb.OrbitalDerivative.derivativeTensorValue_basisTensor line 39
  5. lemma OAI.ContinuumCoulomb.OrbitalDerivative.derivativeTensorValue_occupationTensor line 46
  6. lemma OAI.ContinuumCoulomb.OrbitalDerivative.derivativeTensorValue_memLp line 65
  7. lemma OAI.ContinuumCoulomb.OrbitalDerivative.derivative_bilinear_expansion line 74
  8. lemma OAI.ContinuumCoulomb.OrbitalDerivative.head_derivative_integral line 89
  9. lemma OAI.ContinuumCoulomb.OrbitalDerivative.derivative_CAR_compression line 132
  10. lemma OAI.ContinuumCoulomb.OrbitalDerivative.slater_derivative_CAR_compression line 150