OAI/Analysis/CoulombIonization/ThomasFermi/Pairing.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CoulombAnalysis.tfPairing line 38
  2. lemma OAI.CoulombAnalysis.tfPairing_apply line 41
  3. lemma OAI.CoulombAnalysis.tfPairing_integrable line 48
  4. def OAI.CoulombAnalysis.tfCoulombL line 54
  5. lemma OAI.CoulombAnalysis.tfCoulombL_apply line 58
  6. lemma OAI.CoulombAnalysis.tfCoulomb_integrable line 67
  7. def OAI.CoulombAnalysis.gaussian line 83
  8. lemma OAI.CoulombAnalysis.gaussian_pos line 85
  9. lemma OAI.CoulombAnalysis.gaussian_bound line 87
  10. lemma OAI.CoulombAnalysis.gaussian_continuous line 90
  11. lemma OAI.CoulombAnalysis.gaussian_integral line 97
  12. lemma OAI.CoulombAnalysis.gaussian_integrable line 101
  13. lemma OAI.CoulombAnalysis.gaussian_overlap line 107
  14. lemma OAI.CoulombAnalysis.gaussian_overlap_integral line 116
  15. lemma OAI.CoulombAnalysis.gaussian_overlap_integrable line 122
  16. lemma OAI.CoulombAnalysis.integrable_gaussian_quadratic line 128
  17. lemma OAI.CoulombAnalysis.integrable_gaussian_triple line 137
  18. theorem OAI.CoulombAnalysis.gaussian_quadratic_nonneg line 160
  19. lemma OAI.CoulombAnalysis.coulomb_gaussian_integral line 198
  20. lemma OAI.CoulombAnalysis.coulomb_gaussian_integrable line 208
  21. lemma OAI.CoulombAnalysis.ae_off_diagonal line 219
  22. theorem OAI.CoulombAnalysis.coulomb_quadratic_nonneg line 231
  23. def OAI.CoulombAnalysis.tfExtension line 273
  24. lemma OAI.CoulombAnalysis.tfExtension_integrable line 276
  25. lemma OAI.CoulombAnalysis.tfExtension_direct line 280
  26. lemma OAI.CoulombAnalysis.tfExtension_coulomb_integrable line 288
  27. lemma OAI.CoulombAnalysis.tfCoulombL_extension line 296
  28. lemma OAI.CoulombAnalysis.tfCoulombL_nonneg line 304
  29. lemma OAI.CoulombAnalysis.tfCoulombL_symmetric line 308
  30. lemma OAI.CoulombAnalysis.tfCoulombL_midpoint_gap line 317
  31. def OAI.CoulombAnalysis.tfBallLinear line 326
  32. def OAI.CoulombAnalysis.tfBallFunctional line 330
  33. lemma OAI.CoulombAnalysis.tfBallFunctional_continuous line 333
  34. lemma OAI.CoulombAnalysis.tf_power_dominates_linear line 339
  35. lemma OAI.CoulombAnalysis.tfBallFunctional_lower line 353
  36. lemma OAI.CoulombAnalysis.tfBallFunctional_bddBelow line 362
  37. lemma OAI.CoulombAnalysis.tfBallFunctional_coercive line 375
  38. lemma OAI.CoulombAnalysis.nonnegDensity_smul line 383
  39. lemma OAI.CoulombAnalysis.tfLp_midpoint_gap line 389
  40. lemma OAI.CoulombAnalysis.tfBallFunctional_gap line 405
  41. theorem OAI.CoulombAnalysis.tfBallFunctional_exists_minimizer line 416
  42. lemma OAI.CoulombAnalysis.tfBallFunctional_min_unique line 435
  43. def OAI.CoulombAnalysis.tfPowerDerivative line 453
  44. lemma OAI.CoulombAnalysis.tfPowerDerivative_abs line 455
  45. lemma OAI.CoulombAnalysis.tfPowerDerivative_nonneg line 465
  46. lemma OAI.CoulombAnalysis.hasDerivAt_tfPower line 470
  47. lemma OAI.CoulombAnalysis.tfPowerDerivative_bound line 479