Products of finite measures and probability measures #
This file introduces binary products of finite measures and probability measures. The constructions are obtained from special cases of products of general measures. Taking products nevertheless has specific properties in the cases of finite measures and probability measures, notably the fact that the product measures depend continuously on their factors in the topology of weak convergence when the underlying space is metrizable and separable.
Main definitions #
MeasureTheory.FiniteMeasure.prod
: The product of two finite measures.MeasureTheory.ProbabilityMeasure.prod
: The product of two probability measures.
Main results #
MeasureTheory.ProbabilityMeasure.continuous_prod
: the product probability measure depends
continuously on the factors.
The binary product of finite measures.
Instances For
The binary product of probability measures.
Instances For
The first marginal of a product probability measure is the first probability measure.
The second marginal of a product probability measure is the second probability measure.
The map associating to two probability measures their product is a continuous map.