OAI/Probability/SignedSweeps/MajorizationFactorial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.filter_range_antitone line 9
2. lemma OAI.SignedSweeps.prefix_dominance_excess line 21
3. lemma OAI.SignedSweeps.log_factorial_ramp line 54
4. theorem OAI.SignedSweeps.factorial_product_le_of_prefix_dominance line 87