OAI/Analysis/CoulombRadii/FieldAnalysis/SumSpinDuplicate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.hasSum_spin_duplicate line 91
2. lemma OAI.Coulomb.packetBasis_eigen_nonneg line 103
3. lemma OAI.Coulomb.packetBasis_eigen_le_one line 107
4. lemma OAI.Coulomb.packet_positive_hasSum line 113
5. lemma OAI.Coulomb.packetPositive_density line 124
6. lemma OAI.Coulomb.packetPositive_directional_energy line 150
7. lemma OAI.Coulomb.fermiPacket_positive_kinetic line 162