Sklar's theorem for arbitrary real marginals #
A strictly increasing embedding moves the joint law to the compact unit cube.
Quantile lifting there supplies a copula even when the marginals have atoms.
Uniqueness on marginal CDF ranges is IsSklarCopula.cdf_eq_on_ranges.
theorem
ProbabilityTheory.Copula.exists_sklarCopula
{d : ℕ}
(μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ))
:
∃ (C : Copula d), IsSklarCopula μ C
Every probability law on real vectors admits a Sklar copula.