OAI/Analysis/CoulombRadii/ThomasFermi/Rescaling.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NeutralAtom.scaledDensity line 14
  2. theorem OAI.NeutralAtom.scaledDensity_integrable line 16
  3. theorem OAI.NeutralAtom.integral_scaledDensity line 20
  4. theorem OAI.NeutralAtom.coulombKernel_smul line 27
  5. theorem OAI.NeutralAtom.potentialOf_scaledDensity line 31
  6. theorem OAI.NeutralAtom.screenedField_scaledDensity line 43
  7. theorem OAI.NeutralAtom.WeakNuclearSubsolution.dilate line 51
  8. theorem OAI.NeutralAtom.barrierSource_dilate line 94
  9. theorem OAI.NeutralAtom.WeakNuclearSubsolution.dilate_barrier line 107
  10. theorem OAI.NeutralAtom.scaledDensity_nonneg line 118
  11. theorem OAI.NeutralAtom.scaledDensity_bound line 122
  12. theorem OAI.NeutralAtom.scaledDensity_support line 126
  13. theorem OAI.NeutralAtom.barrier_bounds_dilate line 134
  14. theorem OAI.NeutralAtom.tfDensityScalar_dilate line 160
  15. theorem OAI.NeutralAtom.mul_inverse_power_dilate line 171
  16. theorem OAI.NeutralAtom.screened_comparison_dilate line 176
  17. theorem OAI.NeutralAtom.setIntegral_scaledDensity line 200
  18. theorem OAI.NeutralAtom.smul_spatialAnnulus line 209
  19. theorem OAI.NeutralAtom.annularIntegral_scaledDensity line 221
  20. structure OAI.NeutralAtom.PhysicalRetainedFamily line 226
  21. theorem OAI.NeutralAtom.continuous_scaled_offset line 266
  22. def OAI.NeutralAtom.PhysicalRetainedFamily.toAnalytic line 277