← Copula mathematical handbook

Sklar's theorem for arbitrary laws on the unit cube

noncomputable def ProbabilityTheory.Copula.unitMarginalCDF {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)) (i : Fin d) (x : ↑unitInterval) : ↑unitInterval

The coordinate CDF of a law on the unit cube, with its range bundled in [0,1].

Equations

• ProbabilityTheory.Copula.unitMarginalCDF μ i x = ⟨(MeasureTheory.Measure.map (fun (z : Fin d → ↑unitInterval) => z i) ↑μ).real (Set.Iic x), ⋯⟩

theorem ProbabilityTheory.Copula.exists_sklarCopula_unit {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ↑unitInterval)) : ∃ (C : Copula d), ∀ (x : Fin d → ↑unitInterval), (C.cdf fun (i : Fin d) => unitMarginalCDF μ i (x i)) = (↑μ).real (Set.Iic x)

Every joint law on the unit cube has a Sklar copula, including laws with atoms.