← Mathematical handbook

Sklar's theorem with continuous marginals

The copula is the joint law of the marginal CDF transforms. Equality of lower-orthant probabilities is proved almost everywhere, allowing flat CDFs.

noncomputable def ProbabilityTheory.Copula.marginal {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (i : Fin d) : MeasureTheory.Measure ℝ

A coordinate law of a probability measure on real vectors.

Equations

• ProbabilityTheory.Copula.marginal μ i = MeasureTheory.Measure.map (fun (x : Fin d → ℝ) => x i) ↑μ

instance ProbabilityTheory.Copula.instIsProbabilityMeasureRealMarginal {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (i : Fin d) : MeasureTheory.IsProbabilityMeasure (marginal μ i)

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

Apply each marginal CDF to its own coordinate.

Equations

• ProbabilityTheory.Copula.marginalTransform μ x i = ProbabilityTheory.cdfUnit (ProbabilityTheory.Copula.marginal μ i) (x i)

theorem ProbabilityTheory.Copula.measurable_marginalTransform {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) : Measurable (marginalTransform μ)

theorem ProbabilityTheory.Copula.map_marginalTransform_eval {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) (i : Fin d) : MeasureTheory.Measure.map (fun (x : Fin d → ℝ) => marginalTransform μ x i) ↑μ = MeasureTheory.volume

noncomputable def ProbabilityTheory.Copula.ofContinuousMarginals {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) : Copula d

The copula of a real random vector with continuous marginal CDFs.

Equations

• ProbabilityTheory.Copula.ofContinuousMarginals μ hc = ProbabilityTheory.Copula.ofMap μ (ProbabilityTheory.Copula.marginalTransform μ) ⋯ ⋯

def ProbabilityTheory.Copula.IsSklarCopula {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (C : Copula d) : Prop

The distribution factorization in Sklar's theorem.

Equations

• ProbabilityTheory.Copula.IsSklarCopula μ C = ∀ (x : Fin d → ℝ), C.cdf (ProbabilityTheory.Copula.marginalTransform μ x) = (↑μ).real (Set.Iic x)

theorem ProbabilityTheory.Copula.isSklarCopula_ofContinuousMarginals {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) : IsSklarCopula μ (ofContinuousMarginals μ hc)

theorem ProbabilityTheory.Copula.IsSklarCopula.cdf_eq_on_ranges {d : ℕ} {μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)} {C D : Copula d} (hC : IsSklarCopula μ C) (hD : IsSklarCopula μ D) (u : Fin d → ↑unitInterval) (hu : ∀ (i : Fin d), u i ∈ Set.range (cdfUnit (marginal μ i))) : C.cdf u = D.cdf u

Factorizations agree on the product of marginal CDF ranges, even with atoms.

theorem ProbabilityTheory.Copula.IsSklarCopula.unique {d : ℕ} {μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)} (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) {C D : Copula d} (hC : IsSklarCopula μ C) (hD : IsSklarCopula μ D) : C = D

Continuous marginals make the Sklar copula unique on the entire unit cube.

theorem ProbabilityTheory.Copula.existsUnique_sklarCopula_of_continuous {d : ℕ} (μ : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)) (hc : ∀ (i : Fin d), Continuous ↑(ProbabilityTheory.cdf (marginal μ i))) : ∃! C : Copula d, IsSklarCopula μ C

Existence and uniqueness in Sklar's theorem for continuous marginal CDFs.