OAI/Analysis/CoulombRadii/FieldAnalysis/NormSqSumCosets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.norm_sq_sum_cosets line 64
2. lemma OAI.Coulomb.signed_coset_correlation line 84
3. lemma OAI.Coulomb.norm_sq_signed_sum_cosets line 108
4. lemma OAI.Coulomb.permutation_mul_value line 123
5. lemma OAI.Coulomb.permutation_mul_gradient line 128
6. lemma OAI.Coulomb.permutation_value_covariance line 134
7. lemma OAI.Coulomb.permutation_gradient_covariance line 143
8. def OAI.Coulomb.complexSign line 155
9. lemma OAI.Coulomb.complexSign_sq line 160
10. lemma OAI.Coulomb.complexSign_real line 162
11. lemma OAI.Coulomb.fullAntisymmetrize_gradient line 165
12. lemma OAI.Coulomb.separated_fullAntisymmetrize_value_sq line 170
13. lemma OAI.Coulomb.separated_fullAntisymmetrize_gradient_sq line 206