OAI/Analysis/CoulombRadii/Screening/LogTailMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NeutralAtom.log_probability_fifth line 12
2. lemma OAI.NeutralAtom.probability_of_log_fifth line 27
3. lemma OAI.NeutralAtom.le_discrete_tail_sum line 51
4. lemma OAI.NeutralAtom.firstMoment_le_discrete_tails line 68
5. lemma OAI.NeutralAtom.positive_part_tail line 104
6. theorem OAI.NeutralAtom.logarithmic_tail_integral line 110