OAI/Analysis/CoulombRadii/FormDomain/CubeGradient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.positionCLM_single line 35
2. lemma OAI.Coulomb.tensorOrbital_fderiv line 44
3. lemma OAI.Coulomb.slaterConfiguration_fderiv line 71
4. def OAI.Coulomb.cubeGradient line 91
5. lemma OAI.Coulomb.H1Vector.gradient_spinSpace_memLp line 95
6. lemma OAI.Coulomb.cubeGradient_full_norm line 108
7. lemma OAI.Coulomb.slaterState_cubeGradient line 120
8. lemma OAI.Coulomb.slaterState_kinetic line 133