Repeating probability events

Stream: Is there code for X?

[Gareth Ma]

Is there enough API in Mathlib to formalise that "the expected number of times we have to roll a Fin n-indexed dice before we get a 0 is n times"? If so, can someone point me to some relevant parts of Mathlib? I had no prior experience with probability measure in Mathlib at all.

[Gareth Ma]

I suppose you can formalise a random variable such that $\mathbb{P}[X = k] = \left(1 - \frac{1}{n}\right)^{k - 1} \cdot \frac{1}{n}$, but that kind of loses the point of the problem formulation, which is recursive in nature

[Johan Commelin]

I don't think we have much in this direction if you want to use the probability API. If you take the combinatorics approach, it might be more accessible.