OAI/Analysis/CoulombRadii/FieldAnalysis/CorePerm.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.corePerm line 124
2. lemma OAI.Coulomb.corePerm_left line 128
3. lemma OAI.Coulomb.corePerm_right line 132
4. lemma OAI.Coulomb.corePerm_sign line 136
5. lemma OAI.Coulomb.append_corePerm line 140
6. lemma OAI.Coulomb.permute_core_join line 149
7. lemma OAI.Coulomb.H1Vector.coreSlice_antisymmetric line 163
8. lemma OAI.Coulomb.Antisymmetric.coreSlice line 180
9. lemma OAI.Coulomb.H1Vector.value_eq_zero_of_mass_zero line 184
10. lemma OAI.Coulomb.H1Vector.gradient_eq_zero_of_mass_zero line 195
11. lemma OAI.Coulomb.kinetic_eq_zero_of_mass_zero line 210
12. lemma OAI.Coulomb.kinetic_coreSlice_ae line 218
13. lemma OAI.Coulomb.kinetic_coreSlice_integrable line 226
14. lemma OAI.Coulomb.integral_kinetic_coreSlice line 237
15. def OAI.Coulomb.H1Vector.normalized line 267
16. lemma OAI.Coulomb.mass_normalized line 270
17. lemma OAI.Coulomb.Antisymmetric.normalized line 274
18. lemma OAI.Coulomb.kinetic_normalized_weight line 277
19. lemma OAI.Coulomb.conditional_core_kinetic_identity line 285
20. def OAI.Coulomb.potentialForm line 292
21. lemma OAI.Coulomb.potentialForm_rsmul line 295
22. lemma OAI.Coulomb.potentialForm_eq_zero_of_mass_zero line 301
23. lemma OAI.Coulomb.potentialForm_normalized_weight line 309
24. lemma OAI.Coulomb.potentialForm_coreSlice_ae line 317
25. lemma OAI.Coulomb.potentialForm_coreSlice_integrable line 324
26. lemma OAI.Coulomb.integral_potentialForm_coreSlice line 342