add a type for finite measures

[affeldt-aist]

Motivation for this change

This PR improves the hierarchy of measures as follows:

Rounded boxes were already there.
Finite measures were already there but through the predicate finite_measure only.
Square boxes are new.
Dashed boxes and FinNumFun come with this PR.
AdditiveCharge and Charge come with PR #777 (rebased on this PR)

This PR is necessary to rebase the branch kernels PR #749 because
the latter proves Fubini for s-finite measures which relies
on Fubini for sigma-finite measures which are given
a type using HB which calls for automatic inference
of the type of s-finite measures from the type
of sigma-finite measures.
In the branch kernels we also need to equip the return type of
s-finite kernels with the type of s-finite measures to apply Fubini
for s-finite measures in the proof of commutativity of let-in.

This PR also adde subprobability measures (just to match the hierarchy of kernels)

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

it is also required to rebase PR #749

it looks like rebasing will require a bit more thinking

[hoheinzollern]

This PR is interesting for PR #790, since we need finite measures to prove $L_2 \subset L_1$, which only holds in the case the measure is finite, like with probabilities. See for example here.

[zstone1]

The hierarchy makes sense, but I've got a few questions about HB quirks. But this generally looks good.

[zstone1]

Taking this A : set T is slightly uncomfortable for all of the substructuring reasons we've discussed before.

While building better support for substructures is something we're working on elsewhere. For now it looks like we only use (A := setT) anyway. Is it better to just eliminate A as an argument?

[affeldt-aist]

This is indeed a generality that we do not use, see f4b6571 . It looks fine to me to eliminate it. @CohenCyril ?

[affeldt-aist]

Is it ok to keep both definitions finite_measure and fin_num_fun or should I try to get rid of the former for the latter?

[affeldt-aist]

Is it ok to keep both definitions finite_measure and fin_num_fun or should I try to get rid of the former for the latter?

It seems clearer to get rid of finite_measure and keep fin_num_fun only, see the las commit af15a0c

NB: pr #749 , pr #777 , pr #849 rebase fine so that maybe an ok change

[zstone1]

Happy either way with the extra parameter.

[affeldt-aist]

I have applied a few more comments that I received offline except one requesting a set parameter to fin_num_fun. Is it ok if I issue about it and take care of it later?

[zstone1]

If you're asking me, I think that's fine. It doesn't sound like a big burden to do later, and I'd rather get you unblocked now.

[CohenCyril]

If you're asking me, I think that's fine. It doesn't sound like a big burden to do later, and I'd rather get you unblocked now.

I agree