OAI/Analysis/CoulombRadii/Packets/PacketIndex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Coulomb.packetIndex line 92
2. def OAI.Coulomb.packetBasis line 95
3. instance OAI.Coulomb.packetIndexCountable line 100
4. abbrev OAI.Coulomb.positivePacketIndex line 105
5. lemma OAI.Coulomb.positivePacketIndex_ne_zero line 108
6. lemma OAI.Coulomb.packetPositiveIndex_smooth line 115
7. lemma OAI.Coulomb.orthonormal_representative_inner line 132
8. lemma OAI.Coulomb.spinOrbital_contDiff line 145
9. lemma OAI.Coulomb.spinOrbital_compactSupport line 152
10. lemma OAI.Coulomb.spinOrbital_support line 159
11. lemma OAI.Coulomb.spinOrbital_density line 163
12. lemma OAI.Coulomb.spinOrbital_kinetic line 168