OAI/Probability/ThorpCompatibility/LogEstimates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpCompatibility.sum_reverse_succ line 10
2. lemma OAI.ThorpCompatibility.sum_log_sub line 18
3. lemma OAI.ThorpCompatibility.sum_inv_sub line 25
4. lemma OAI.ThorpCompatibility.log_step_lower line 31
5. lemma OAI.ThorpCompatibility.log_factorial_upper line 41
6. lemma OAI.ThorpCompatibility.neg_log_add_lower line 58
7. lemma OAI.ThorpCompatibility.average_log_rank_lower line 67
8. lemma OAI.ThorpCompatibility.average_inverse_rank line 85