OAI/Analysis/CoulombIonization/ThomasFermi/SommerfeldCoefficient.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombPDE.lower_barrier_laplacian line 31
2. theorem OAI.CoulombPDE.singular_upper_bound line 74
3. theorem OAI.CoulombPDE.singular_lower_bound line 128
4. def OAI.CoulombPDE.sommerfeldCoefficient line 184
5. lemma OAI.CoulombPDE.sommerfeldCoefficient_pos line 186
6. lemma OAI.CoulombPDE.sommerfeldCoefficient_half line 190
7. lemma OAI.CoulombPDE.norm_four_mul_radialPower line 198
8. theorem OAI.CoulombPDE.sommerfeld_asymptotic line 204
9. structure OAI.CoulombPDE.SingularProfile line 258
10. lemma OAI.CoulombPDE.SingularProfile.asymptotic line 266
11. lemma OAI.CoulombPDE.reaction_superlinear line 273
12. lemma OAI.CoulombPDE.deleted_eventually_to_small_ball line 297
13. theorem OAI.CoulombPDE.global_punctured_maximum_principle line 307
14. lemma OAI.CoulombPDE.SingularProfile.scaled_comparison line 320
15. theorem OAI.CoulombPDE.singular_profile_unique line 365
16. lemma OAI.CoulombPDE.laplacian_comp_isometry line 383
17. lemma OAI.CoulombPDE.SingularProfile.comp_isometry line 397
18. theorem OAI.CoulombPDE.SingularProfile.rotation_invariant line 417
19. theorem OAI.CoulombPDE.SingularProfile.radial line 422