OAI/Analysis/CoulombRadii/RadialBounds/Radial.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.IsRadial line 13
  2. theorem OAI.NeutralAtom.potentialOf_isometry line 15
  3. theorem OAI.NeutralAtom.potentialOf_radial line 26
  4. theorem OAI.NeutralAtom.radial_potential_le_center line 34
  5. theorem OAI.NeutralAtom.integrable_coulomb_pairing line 65
  6. theorem OAI.NeutralAtom.coulomb_pairing_comm line 107
  7. theorem OAI.NeutralAtom.neutral_radial_average_nonneg line 124
  8. theorem OAI.NeutralAtom.neutral_weighted_lone_bound line 160
  9. theorem OAI.NeutralAtom.neutral_annulus_lone_bound line 199
  10. theorem OAI.NeutralAtom.locallyUniform_subsequence_of_equicontinuous line 251
  11. theorem OAI.NeutralAtom.equicontinuous_of_eventual_local_lipschitz line 286
  12. theorem OAI.NeutralAtom.norm_bounded_of_eventually_bounded line 312
  13. theorem OAI.NeutralAtom.locallyUniform_subsequence_of_eventual_ball_estimates line 325
  14. def OAI.NeutralAtom.screenedField line 363
  15. theorem OAI.NeutralAtom.screenedField_continuousOn line 366
  16. theorem OAI.NeutralAtom.screenedField_weakLaplacian line 375
  17. theorem OAI.NeutralAtom.isCompact_closedNormAnnulus line 403