Laws on real vectors are determined by their distribution functions #
Lower orthants generate the Borel sigma algebra of Fin d → ℝ and form a pi-system of boxes.
This is the real-valued analogue of Copula.ext_cdf and is used for the random-variable
versions of Nelsen, An Introduction to Copulas, second edition, §2.4, §2.7 and §3.3.
theorem
ProbabilityTheory.Copula.ext_real_of_Iic
{d : ℕ}
{μ ν : MeasureTheory.Measure (Fin d → ℝ)}
[MeasureTheory.IsProbabilityMeasure μ]
[MeasureTheory.IsProbabilityMeasure ν]
(h : ∀ (x : Fin d → ℝ), μ.real (Set.Iic x) = ν.real (Set.Iic x))
:
Two probability measures on Fin d → ℝ with the same lower-orthant probabilities agree.