OAI/Analysis/CoulombRadii/ThomasFermi/TFNonneg.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.TFNonneg line 22
  2. lemma OAI.Coulomb.tfNonneg_zero line 23
  3. lemma OAI.Coulomb.TFNonneg.add line 28
  4. lemma OAI.Coulomb.TFNonneg.smul line 31
  5. lemma OAI.Coulomb.tfNonneg_closed line 34
  6. lemma OAI.Coulomb.tfLp_nonneg_power line 40
  7. lemma OAI.Coulomb.tfLp_midpoint_power line 46
  8. def OAI.Coulomb.tfOne line 53
  9. lemma OAI.Coulomb.tfOne_coe line 55
  10. lemma OAI.Coulomb.tfNonneg_one line 57
  11. lemma OAI.Coulomb.tfLp_gap_nonneg line 60
  12. lemma OAI.Coulomb.tfLp_midpoint_gap line 73
  13. lemma OAI.Coulomb.tfExtend_add_ae line 107
  14. lemma OAI.Coulomb.tfExtend_smul_ae line 114
  15. lemma OAI.Coulomb.tfCoulomb_symm line 121
  16. lemma OAI.Coulomb.tfCoulomb_add_left line 130
  17. lemma OAI.Coulomb.tfCoulomb_smul_left line 142
  18. lemma OAI.Coulomb.tfCoulomb_bound line 154
  19. def OAI.Coulomb.tfCoulombLinear line 187
  20. def OAI.Coulomb.tfCoulombContinuous line 194
  21. lemma OAI.Coulomb.tfCoulomb_continuous line 200