OAI/Probability/ThorpCompatibility/FactorialBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpCompatibility.log_step_bound line 9
2. lemma OAI.ThorpCompatibility.log_descFactorial_integral line 25
3. lemma OAI.ThorpCompatibility.log_descFactorial_lower line 46
4. lemma OAI.ThorpCompatibility.descFactorial_exponential_lower line 59