OAI/Analysis/CoulombRadii/FieldAnalysis/Field.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.RetainedAnalyticSequence.field line 14
  2. def OAI.NeutralAtom.RetainedAnalyticSequence.reindex line 17
  3. def OAI.NeutralAtom.sommerfeldProfile line 52
  4. def OAI.NeutralAtom.sommerfeldDensity line 54
  5. theorem OAI.NeutralAtom.sommerfeldProfile_continuousOn line 56
  6. theorem OAI.NeutralAtom.sommerfeldProfile_density line 61
  7. theorem OAI.NeutralAtom.RetainedAnalyticSequence.limit_eq_profile line 69
  8. theorem OAI.NeutralAtom.RetainedAnalyticSequence.precompact line 99
  9. theorem OAI.NeutralAtom.RetainedAnalyticSequence.converges line 111
  10. theorem OAI.NeutralAtom.uniformOn_of_selected_locallyUniformly line 128
  11. structure OAI.NeutralAtom.RetainedAnalyticFamily line 154
  12. def OAI.NeutralAtom.RetainedAnalyticFamily.select line 192
  13. theorem OAI.NeutralAtom.RetainedAnalyticFamily.uniform line 228
  14. theorem OAI.NeutralAtom.sommerfeldDensity_continuousOn line 245
  15. theorem OAI.NeutralAtom.RetainedAnalyticFamily.uniform_integral line 250
  16. theorem OAI.NeutralAtom.expectation_tendsto_of_eventual_uniform line 272
  17. theorem OAI.NeutralAtom.integrable_sommerfeldDensity_exterior line 297
  18. theorem OAI.NeutralAtom.sommerfeldDensity_exteriorMass line 303
  19. theorem OAI.NeutralAtom.sommerfeldDensity_annularMass line 313
  20. theorem OAI.NeutralAtom.RetainedAnalyticFamily.expected_integral line 336
  21. theorem OAI.NeutralAtom.RetainedAnalyticFamily.expected_annulus line 357