add variant of Fubini lemmas and rename to clarify

[affeldt-aist]

Motivation for this change

When working on the sampling branch, we realized that we need variants of existing Fubini lemmas but adding these variants was no compatible with the current naming scheme. This PR introduces the variants and change the naming scheme to something easier to comprehend.

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

[t6s]

The new names are terrible, but since they are longer, it is easy to note where those terrible names occur. I think therefore this PR is good.

By the way, I noticed that the header comment contains typos "measure measure".

Suggestions for future changes:
We will not need to maintain two definitions of product measures as first-class; instead we can define the product measure by sval ("existence of an extension that satisfies μ(A x B) = μ1(A)μ2(B)").
In many cases where both μ1 and μ2 are σ-finite (Section fubini, for example), this definition will not cause problems thanks to the uniqueness lemmas.
product_measure1 and product_measure2 in the current code then should be given more specific name, possibly along with other definitions of a product measure (https://math.stackexchange.com/questions/70888/uniqueness-of-product-measure-non-sigma-finite-case).