Rémy Degenne

Could `summable_of_sum_range_le` be also generalized in some way, such that the same lemma would work for both real and nnreal? If it gets complicated and you don't want to investigate...

Yeah, ennreal looks different. I was only talking about real and nnreal. The PR looks good. I let you decide whether you merge as it is now or not. bors...

bors r+

I was definitely planning to add Azuma-Hoeffding at some point. But I can change this PR to do it now, no problem. About bounded vs sub-Gaussian random variables: the proof...

Update on this: I will introduce a more general property stating that a random variable has its cgf bounded from above by some function (or the same on the mgf,...

bors r+

The non-mathematical reason I added that hypothesis is that I used `measurable_from_prod_countable` (in the file `Probability.Kernel.Disintegration.Basic`). It asked for that typeclass and I added it without thinking about it.

I don't see how I could remove the `MeasurableSingletonClass` assumption without adding another assumption somewhere. To conclude that everything is constant on the atoms, I would need the codomain to...

@sgouezel All prerequisites are now merged (thanks for the reviews!), and this is the final disintegration PR. I did not resolve your question about the `MeasurableSetSingleton` hypothesis: if you have...

Thanks for the help! Your code looks good. I saw a place where I think I can refactor my code to improve its clarity, so I'm turning that PR back...