Functions and prob. distributions

Stream: mathlib4

[Martin Dvořák]

How much tools do we have for functions that work with probability distributions?
In particular, I would like to work with:

• functions from $A^k$ to fin-sup probability distribution over $A$
• lifting functions $A \rightarrow A$ to unary operations on fin-sup probability distributions over $A$