OAI/Analysis/CoulombRadii/Variational/ConfigurationDensity.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NeutralAtom.largeCharge_eq_atTop line 15
2. theorem OAI.NeutralAtom.bTF_pos line 21
3. theorem OAI.NeutralAtom.density_nonneg line 26
4. theorem OAI.NeutralAtom.exteriorMass_nonneg line 32
5. theorem OAI.NeutralAtom.radius_nonneg line 36
6. theorem OAI.NeutralAtom.integrable_cons line 42
7. theorem OAI.NeutralAtom.integral_cons line 52
8. theorem OAI.NeutralAtom.integrable_density line 63
9. theorem OAI.NeutralAtom.integral_density line 70
10. theorem OAI.NeutralAtom.groundState_integral_density line 82
11. theorem OAI.NeutralAtom.exteriorMass_antitone line 88
12. theorem OAI.NeutralAtom.exteriorMass_tendsto_zero line 95
13. theorem OAI.NeutralAtom.radius_set_nonempty line 112
14. theorem OAI.NeutralAtom.radius_bracket line 120
15. theorem OAI.NeutralAtom.scaled_ereal_bounds line 135
16. theorem OAI.NeutralAtom.inner_limits_bracket line 147
17. theorem OAI.NeutralAtom.tendsto_ereal_of_eventual_brackets line 173
18. theorem OAI.NeutralAtom.iterated_limits_of_radius_brackets line 192
19. theorem OAI.NeutralAtom.inverse_comparison_inversion line 218
20. theorem OAI.NeutralAtom.uniform_threshold_of_sequential line 275
21. theorem OAI.NeutralAtom.cube_root_cube line 299
22. theorem OAI.NeutralAtom.bTF_cube line 303
23. theorem OAI.NeutralAtom.normalized_tail_scale line 309
24. theorem OAI.NeutralAtom.inverse_comparison_fixed_accuracy line 315
25. def OAI.NeutralAtom.configurationDensity line 348
26. def OAI.NeutralAtom.rawExpectation line 351
27. def OAI.NeutralAtom.rawCount line 354
28. theorem OAI.NeutralAtom.configurationDensity_nonneg line 357
29. theorem OAI.NeutralAtom.integrable_configurationDensity line 360
30. theorem OAI.NeutralAtom.integral_configurationDensity line 364
31. theorem OAI.NeutralAtom.piCongrLeft_perm line 369
32. theorem OAI.NeutralAtom.configurationDensity_perm line 374