OAI/Analysis/CoulombRadii/FieldAnalysis/Gaussian.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.gaussian line 13
  2. lemma OAI.Coulomb.gaussian_pos line 14
  3. lemma OAI.Coulomb.gaussian_le_one line 15
  4. lemma OAI.Coulomb.gaussian_continuous line 18
  5. lemma OAI.Coulomb.gaussian_integrable line 19
  6. lemma OAI.Coulomb.gaussian_integral line 26
  7. lemma OAI.Coulomb.kernel_gaussian_integral line 29
  8. lemma OAI.Coulomb.gaussian_product line 39
  9. lemma OAI.Coulomb.gaussian_product_integrable line 51
  10. lemma OAI.Coulomb.gaussian_convolution_identity line 56
  11. lemma OAI.Coulomb.integrable_gaussian_weight line 62
  12. lemma OAI.Coulomb.integrable_gaussian_pair line 71
  13. lemma OAI.Coulomb.gaussian_square_integrable line 82
  14. lemma OAI.Coulomb.gaussian_form_nonneg line 105
  15. lemma OAI.Coulomb.space_ae_distinct line 130
  16. lemma OAI.Coulomb.gaussian_parameter_integrable line 139
  17. lemma OAI.Coulomb.gaussian_parameter_integral line 148
  18. lemma OAI.Coulomb.coulomb_gaussian_integrable_of_pair line 157
  19. lemma OAI.Coulomb.coulomb_form_nonneg_of_pair line 178
  20. lemma OAI.Coulomb.coulomb_lp_form_nonneg line 200