OAI/Analysis/CoulombIonization/ThomasFermi/TfPowerIntegralDeriv.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CoulombAnalysis.tf_power_integral_hasDerivAt line 44
  2. lemma OAI.CoulombAnalysis.tfPowerDerivative_mul_integrable line 71
  3. lemma OAI.CoulombAnalysis.tfLp_kinetic_hasDerivAt line 82
  4. lemma OAI.CoulombAnalysis.tfBallFunctional_hasDerivAt line 100
  5. lemma OAI.CoulombAnalysis.hasDerivAt_nonneg_of_right_min line 121
  6. lemma OAI.CoulombAnalysis.tfBallFunctional_variation_nonneg line 128
  7. lemma OAI.CoulombAnalysis.tfBallFunctional_variation_self line 138
  8. def OAI.CoulombAnalysis.tfBallPotential line 152
  9. lemma OAI.CoulombAnalysis.tfBallPotential_integrable line 155
  10. lemma OAI.CoulombAnalysis.tfCoulombL_potential line 166
  11. lemma OAI.CoulombAnalysis.tfBallPotential_mul_integrable line 177
  12. def OAI.CoulombAnalysis.tfBallGradient line 189
  13. lemma OAI.CoulombAnalysis.tfBallGradient_integrable line 192
  14. lemma OAI.CoulombAnalysis.tfBallGradient_mul_integrable line 200
  15. lemma OAI.CoulombAnalysis.tfBallGradient_pair line 208
  16. lemma OAI.CoulombAnalysis.tfBallGradient_nonneg line 227
  17. lemma OAI.CoulombAnalysis.tfBallGradient_complementarity line 250
  18. theorem OAI.CoulombAnalysis.tfBallFunctional_euler line 261