OAI/Analysis/CoulombRadii/Variational/PuncturedPosition.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NeutralAtom.closedBall_eighth_subset_annulus line 14
  2. theorem OAI.NeutralAtom.neutral_screened_ball_estimates line 25
  3. abbrev OAI.NeutralAtom.PuncturedPosition line 70
  4. def OAI.NeutralAtom.extendPunctured line 72
  5. theorem OAI.NeutralAtom.extendPunctured_val line 75
  6. theorem OAI.NeutralAtom.neutral_screened_precompact_sequence line 78
  7. theorem OAI.NeutralAtom.tendsto_integral_mul_test_of_locallyUniformlyOn line 125
  8. theorem OAI.NeutralAtom.continuous_comp_locallyUniformlyOn line 153
  9. theorem OAI.NeutralAtom.HasWeakLaplacian.locallyUniformLimit line 171
  10. def OAI.NeutralAtom.tfDensityScalar line 188
  11. theorem OAI.NeutralAtom.tfDensityScalar_continuous line 190
  12. theorem OAI.NeutralAtom.density_locallyUniform_of_vanishing_error line 194
  13. theorem OAI.NeutralAtom.screened_semilinear_limit line 205
  14. theorem OAI.NeutralAtom.poisson_interior_estimates_uniform line 230
  15. theorem OAI.NeutralAtom.tendsto_integral_norm_on_compact_of_locallyUniformlyOn line 344
  16. def OAI.NeutralAtom.closedNormAnnulus line 367
  17. theorem OAI.NeutralAtom.smul_closedNormAnnulus line 369
  18. theorem OAI.NeutralAtom.volume_closedNormAnnulus_dilate line 383
  19. theorem OAI.NeutralAtom.dilate_annular_lone_bound line 393
  20. theorem OAI.NeutralAtom.neutral_screened_limit_annular_lone line 411