OAI/Analysis/CoulombRadii/FieldAnalysis/PotentialAddRsmul.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.potential_add_rsmul line 14
  2. lemma OAI.Coulomb.nuclearEnergy_add_rsmul line 39
  3. lemma OAI.Coulomb.pairEnergy_add_rsmul line 48
  4. lemma OAI.Coulomb.form_add_rsmul line 56
  5. lemma OAI.Coulomb.linear_term_zero_of_eventually_quadratic_nonneg line 65
  6. lemma OAI.Coulomb.GroundState.polarization line 90
  7. lemma OAI.Coulomb.norm_double_multiplier_identity line 119
  8. lemma OAI.Coulomb.norm_double_mass_identity line 128
  9. lemma OAI.Coulomb.integral_quadratic_expansion line 135
  10. lemma OAI.Coulomb.mass_double_smoothMul line 145
  11. lemma OAI.Coulomb.potential_double_smoothMul line 176
  12. lemma OAI.Coulomb.kinetic_double_smoothMul line 205
  13. lemma OAI.Coulomb.nuclearEnergy_double_smoothMul line 240
  14. lemma OAI.Coulomb.pairEnergy_double_smoothMul line 256
  15. lemma OAI.Coulomb.form_double_smoothMul line 271
  16. theorem OAI.Coulomb.GroundState.smooth_multiplier_identity line 286