OAI/Analysis/CoulombRadii/Localization/ThinCut.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.transition_derivative_compact line 13
  2. lemma OAI.Coulomb.transition_derivative_bounded line 30
  3. def OAI.Coulomb.transitionDerivativeBound line 36
  4. lemma OAI.Coulomb.transitionDerivativeBound_pos line 37
  5. lemma OAI.Coulomb.transition_derivative_bound line 39
  6. def OAI.Coulomb.thinAngle line 42
  7. lemma OAI.Coulomb.thinAngle_smooth line 45
  8. lemma OAI.Coulomb.thinAngle_fderiv line 49
  9. lemma OAI.Coulomb.thinAngle_core line 68
  10. lemma OAI.Coulomb.thinAngle_exterior line 77
  11. lemma OAI.Coulomb.thinAngle_fderiv_exterior line 84
  12. def OAI.Coulomb.thinCutCoefficient line 94
  13. lemma OAI.Coulomb.thinCutCoefficient_pos line 95
  14. lemma OAI.Coulomb.thinAngle_derivative_bound line 97
  15. def OAI.Coulomb.thinCut line 121
  16. lemma OAI.Coulomb.thinCut_smooth line 123
  17. lemma OAI.Coulomb.thinCut_partition line 128
  18. lemma OAI.Coulomb.thinCut_core_zero line 130
  19. lemma OAI.Coulomb.thinCut_out_zero line 133
  20. lemma OAI.Coulomb.thinCut_derivative_bound line 136