OAI/Analysis/CoulombRadii/FieldAnalysis/TsumFixed.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.tsum_fixed_zero line 10
2. lemma OAI.Coulomb.basis_contraction_pauli line 26
3. lemma OAI.Coulomb.unit_contraction_pauli line 56
4. lemma OAI.Coulomb.fiberContract_const_mul line 89
5. lemma OAI.Coulomb.contraction_pauli line 97
6. lemma OAI.Coulomb.orbital_orthonormal line 144
7. lemma OAI.Coulomb.orbital_sum_memLp line 151
8. lemma OAI.Coulomb.orbital_sum_toLp line 155
9. lemma OAI.Coulomb.orbital_sum_sq line 175
10. def OAI.Coulomb.lowOrbital line 191
11. lemma OAI.Coulomb.lowOrbital_memLp line 195
12. lemma OAI.Coulomb.lowOrbital_sq line 199