Lifting joint laws through marginal sampling maps #
theorem
ProbabilityTheory.Copula.exists_lift
{d : ℕ}
{B : Type u_1}
[MeasurableSpace B]
[StandardBorelSpace B]
[Nonempty B]
(μ : MeasureTheory.ProbabilityMeasure (Fin d → B))
(q : Fin d → ↑unitInterval → B)
(hq : ∀ (i : Fin d), Measurable (q i))
(hqm :
∀ (i : Fin d),
MeasureTheory.Measure.map (q i) MeasureTheory.volume = MeasureTheory.Measure.map (fun (x : Fin d → B) => x i) ↑μ)
:
∃ (C : Copula d), MeasureTheory.Measure.map (fun (u : Fin d → ↑unitInterval) (i : Fin d) => q i (u i)) C.toMeasure = ↑μ
If each coordinate law can be sampled from a uniform variable, a joint law can be lifted to a copula through those sampling maps.