OAI/Analysis/CoulombRadii/FormDomain/H1Pairing.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.real_inner_norm_algebra line 14
  2. lemma OAI.Coulomb.weighted_inner_integrable line 17
  3. lemma OAI.Coulomb.integral_weighted_inner line 27
  4. def OAI.Coulomb.massPair line 45
  5. def OAI.Coulomb.kineticPair line 46
  6. def OAI.Coulomb.nuclearPair line 47
  7. def OAI.Coulomb.repulsionPair line 49
  8. def OAI.Coulomb.formPair line 51
  9. lemma OAI.Coulomb.massPair_polarization line 52
  10. lemma OAI.Coulomb.kineticPair_polarization line 62
  11. lemma OAI.Coulomb.nuclearPair_polarization line 75
  12. lemma OAI.Coulomb.repulsionPair_polarization line 82
  13. lemma OAI.Coulomb.formPair_polarization line 89
  14. lemma OAI.Coulomb.formPair_kinetic_integrable line 93
  15. lemma OAI.Coulomb.formPair_nuclear_integrable line 96
  16. lemma OAI.Coulomb.formPair_repulsion_integrable line 99
  17. lemma OAI.Coulomb.form_ge_sector_bottom line 103
  18. lemma OAI.Coulomb.sector_minimizer_weak_eigen line 114
  19. lemma OAI.Coulomb.integrable_real_bounded_mul line 145
  20. lemma OAI.Coulomb.reciprocal_kinetic_nonneg line 150