improve the interface for the product measure

[affeldt-aist]

from the conversion of PR #1651

"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)."

@t6s