OAI/Analysis/CoulombRadii/Localization/RadialCut.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.cutSeed line 13
  2. lemma OAI.Coulomb.cutSeed_smooth line 14
  3. lemma OAI.Coulomb.cutSeed_one line 16
  4. lemma OAI.Coulomb.cutSeed_zero line 19
  5. lemma OAI.Coulomb.cutSeed_compact line 22
  6. lemma OAI.Coulomb.cutSeed_derivative_bounded line 27
  7. def OAI.Coulomb.cutSeedDerivativeBound line 31
  8. lemma OAI.Coulomb.cutSeedDerivativeBound_pos line 32
  9. lemma OAI.Coulomb.norm_cutSeed_derivative line 33
  10. def OAI.Coulomb.cutAngle line 36
  11. lemma OAI.Coulomb.cutAngle_smooth line 37
  12. lemma OAI.Coulomb.cutAngle_fderiv line 40
  13. def OAI.Coulomb.radialCut line 55
  14. lemma OAI.Coulomb.radialCut_smooth line 57
  15. lemma OAI.Coulomb.radialCut_partition line 62
  16. lemma OAI.Coulomb.radialCut_core_zero line 65
  17. lemma OAI.Coulomb.radialCut_out_zero line 71
  18. def OAI.Coulomb.radialCutCoefficient line 78
  19. lemma OAI.Coulomb.radialCutCoefficient_pos line 79
  20. lemma OAI.Coulomb.radialCut_derivative_bound line 81
  21. lemma OAI.Coulomb.radialCut_fderiv_zero line 108
  22. lemma OAI.Coulomb.radialCut_gradient_bound line 121
  23. def OAI.Coulomb.expectedPopulation line 139
  24. lemma OAI.Coulomb.population_integrable line 142
  25. theorem OAI.Coulomb.form_radial_labelCut line 151