OAI/Analysis/CoulombIonization/RadialBounds/Radial.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAnalysis.IsRadial line 57
  2. lemma OAI.CoulombAnalysis.tfPotential_radial line 59
  3. lemma OAI.CoulombAnalysis.tfPotential_compact_bound line 69
  4. lemma OAI.CoulombAnalysis.tfPotential_compact_mass_bound line 92
  5. lemma OAI.CoulombAnalysis.tfPotential_compact_decay line 132
  6. lemma OAI.CoulombAnalysis.tfPotential_harmonic_outside line 154
  7. theorem OAI.CoulombAnalysis.tfPotential_newton_exterior line 166
  8. lemma OAI.CoulombAnalysis.tfPotential_harmonic_inside line 232
  9. theorem OAI.CoulombAnalysis.tfPotential_newton_interior line 244
  10. lemma OAI.CoulombAnalysis.tfPotential_newton_exterior_closed line 294
  11. lemma OAI.CoulombAnalysis.IsRadial.indicator_norm_le line 311
  12. lemma OAI.CoulombAnalysis.IsRadial.indicator_norm_gt line 316
  13. theorem OAI.CoulombAnalysis.tfPotential_newton line 321