add poisson distribution

[IshiguroYoshihiro]

Motivation for this change

Adding Poisson distribution.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Very welcomed addition!

esum_limn_ge0 can actually be proved as follows:

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Variables (R : realType).
Context {f : nat -> R}.
Hypothesis (f0 : forall n, 0 <= f n).

Lemma esum_limn_ge0 :
 \esum_(i in [set: nat]) (f i)%:E
  = limn
      (EFin \o (fun n : nat => (\sum_(0 <= k < n) f k)%R)).
Proof.
rewrite -set_true -nneseries_esum//; last by move=> *; rewrite lee_fin.
by apply/congr_lim/funext => n/=; rewrite -sumEFin.
Qed.

End elim_limn_ge0.

which suggests that the lemma is moderately useful.
In fact, it is a bit shorter to prove poisson_setT
by moving from esum to nneseries where there are
more lemmas (and this proof does not require esum_limn_ge0).
I have therefore removed it.
On the other hand, this also suggests that nneseries_esum
is a bit awkward to use when use with the whole set, I have
therefore added the technical lemma nneseries_esumT
and this helps a bit imo.