OAI/Analysis/CoulombRadii/Screening/AtomicBudgetScreening.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Coulomb.atomicBudgetRawValues line 14
  2. def OAI.Coulomb.atomicBudgetRawSup line 19
  3. lemma OAI.Coulomb.atomicBudgetRawValues_nonempty line 22
  4. lemma OAI.Coulomb.atomicBudgetRawValues_cap line 25
  5. lemma OAI.Coulomb.atomicBudgetRawValues_bdd line 45
  6. lemma OAI.Coulomb.atomicBudgetRawSup_nonneg line 49
  7. lemma OAI.Coulomb.atomicBudgetRawSup_cap line 54
  8. theorem OAI.Coulomb.AtomicBudgetHistory.append_normalized line 59
  9. def OAI.Coulomb.atomicBudgetRecursionA line 134
  10. def OAI.Coulomb.atomicBudgetRecursionC line 139
  11. lemma OAI.Coulomb.atomicBudgetRecursionC_ge_four line 141
  12. lemma OAI.Coulomb.AtomicBudgetHistory.rawSquare_le_next_sup line 146
  13. lemma OAI.Coulomb.atomicBudgetRawValues_recursion line 170
  14. theorem OAI.Coulomb.atomicBudgetRawSup_recursion line 218
  15. theorem OAI.Coulomb.atomicBudgetRawSup_uniform line 238
  16. theorem OAI.Coulomb.AtomicBudgetHistory.positive_field line 256
  17. theorem OAI.Coulomb.AtomicBudgetHistory.positive_field_actual_counts line 273