`OAI/NumberTheory/Ostmann/Preliminaries/FallingFactorialError.lean`

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The elementary collision loss for sampling distinct indices

theorem OAI.Ostmann.pow_le_descFactorial_add line 11
Source documentation
A convenient collision bound with no restriction that k be smaller than J.
```
theorem pow_le_descFactorial_add (J : ℕ) (hJ : 1 ≤ J) (k : ℕ) :
    J ^ k ≤ J.descFactorial k + k ^ 2 * J ^ (k - 1) := by
…
```