OAI/Analysis/CoulombIonization/RadialBounds/WeakSingularProfileBarrier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CoulombAnalysis.WeakSingularProfile line 21
  2. lemma OAI.CoulombAnalysis.WeakSingularProfile.of_classical line 29
  3. lemma OAI.CoulombAnalysis.WeakSingularProfile.asymptotic line 35
  4. lemma OAI.CoulombAnalysis.WeakSingularProfile.scaled_comparison line 42
  5. theorem OAI.CoulombAnalysis.weak_singular_profile_unique line 91
  6. theorem OAI.CoulombAnalysis.weak_profile_eq_tfInfiniteField line 109
  7. theorem OAI.CoulombAnalysis.weak_profile_classical line 115
  8. lemma OAI.CoulombAnalysis.weak_profile_of_cap_barrier line 136
  9. lemma OAI.CoulombAnalysis.tfInfiniteRadial_exterior line 165
  10. lemma OAI.CoulombAnalysis.tfInfiniteField_exterior line 174
  11. lemma OAI.CoulombAnalysis.tfInfiniteField_sphereMean line 177
  12. theorem OAI.CoulombAnalysis.weak_profile_charge_eq line 181
  13. theorem OAI.CoulombAnalysis.weak_limit_identification line 203