OAI/Analysis/CoulombRadii/FormDomain/Add.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.blockRadiusSq_nuclear line 14
2. lemma OAI.Coulomb.blockRadiusSq_pair line 19
3. lemma OAI.Coulomb.hardyCoulomb_nuclear line 24
4. lemma OAI.Coulomb.hardyCoulomb_pair line 29
5. lemma OAI.Coulomb.H1Vector.nuclear_coulomb_integrable_bound line 35
6. lemma OAI.Coulomb.H1Vector.pair_coulomb_integrable_bound line 44
7. lemma OAI.Coulomb.H1Vector.nuclear_integrable line 53
8. lemma OAI.Coulomb.H1Vector.pair_integrable line 64
9. lemma OAI.Coulomb.potential_smooth_partition line 79
10. lemma OAI.Coulomb.nuclearEnergy_smooth_partition line 98
11. lemma OAI.Coulomb.pairEnergy_smooth_partition line 113
12. theorem OAI.Coulomb.form_smooth_partition line 127
13. lemma OAI.Coulomb.mass_nonneg line 143
14. lemma OAI.Coulomb.kinetic_nonneg line 146
15. lemma OAI.Coulomb.pairEnergy_nonneg line 151
16. lemma OAI.Coulomb.totalCharge_ge_card line 165
17. lemma OAI.Coulomb.totalCharge_pos line 170
18. lemma OAI.Coulomb.nuclearEnergy_eq_sum line 173
19. lemma OAI.Coulomb.nuclearEnergy_bound line 191
20. lemma OAI.Coulomb.form_lower_bound line 236
21. lemma OAI.Coulomb.sector_forms_bddBelow line 255
22. lemma OAI.Coulomb.energy_le_form line 263
23. lemma OAI.Coulomb.GroundState.minimizes line 268
24. lemma OAI.Coulomb.H1Vector.test_integrable line 274
25. def OAI.Coulomb.H1Vector.add line 283
26. def OAI.Coulomb.H1Vector.rsmul line 306
27. lemma OAI.Coulomb.Antisymmetric.add line 316
28. lemma OAI.Coulomb.Antisymmetric.rsmul line 324
29. lemma OAI.Coulomb.mass_rsmul line 333
30. lemma OAI.Coulomb.kinetic_rsmul line 338
31. lemma OAI.Coulomb.nuclearEnergy_rsmul line 344
32. lemma OAI.Coulomb.pairEnergy_rsmul line 351
33. lemma OAI.Coulomb.form_rsmul line 358
34. lemma OAI.Coulomb.energy_mul_mass_le_form line 363
35. lemma OAI.Coulomb.norm_add_rsmul_sq line 376
36. lemma OAI.Coulomb.mass_add_rsmul line 384
37. lemma OAI.Coulomb.kinetic_add_rsmul line 408